Глава
On the expressive power of some extensions of Linear Temporal Logic
В книге
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя среда воздействует на систему, и откликов (действий), которые вырабатывает или исполняет система в ответ на внешние воздействия. Поэтому при верификации некоторых видов реагирующих систем элементарными свойствами становятся множества конечных последовательностей действий. Это обстоятельство должно быть также учтено при разработке формального языка спецификаций поведения таких систем. В данной статье рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преоб\-разователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени LTL. В этой работе рассматривается новый язык формальных спецификаций LP-LTL, представляющий собой расширение темпоральной логики LTL, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах LP-LTL снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах LP-LTL также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик LP-LTL и LP-CTL. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики LP-LTL и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике LP-LTL были выделены два фрагмента LP-1-LTL и LP-n-LTL. Нам удалось установить, что язык спецификаций LP-1-LTL более выразителен, чем LTL, в то время как фрагмент LP-n-LTL обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S1S.
This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же статье было показано, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях, работающих над свободными полугруппами, разрешима со сложностью по времени, оцениваемой двойной экспонентой от размера проверяемой формулы.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 invited talks in full paper length. The papers cover various topics in the field of Petri nets and related models of concurrency.
This volume constitutes the refereed proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science, MFCS 2012, held in Bratislava, Slovakia, in August 2012. The 63 revised full papers presented together with 8 invited talks were carefully reviewed and selected from 162 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence.