Preview

Моделирование и анализ информационных систем

Расширенный поиск

LTL-спецификация счётчиковых машин

https://doi.org/10.18255/1818-1015-2021-1-104-119

Полный текст:

Аннотация

Статья написана в поддержку учебной дисциплины “Неклассические логики”. В рамках этой дисциплины объектами изучения являются базовые принципы и конструктивные элементы, с помощью которых происходит формальное построение различных неклассических логик высказываний. Несмотря на абстрактность теории неклассических логик, в которой основное внимание уделяется строгой математической формализации логических рассуждений, существуют реальные прикладные области применения теоретических результатов. В частности, языки темпоральных модальных логик широко используются для моделирования, спецификации и верификации (анализа корректности) программных систем логического управления. В этой статье на примере линейной темпоральной логики LTL демонстрируется, как абстрактные понятия неклассических логик могут находить отражение на практике в области информационных технологий и программирования. Показывается возможность представления поведения программной системы в виде набора LTL-формул и использования этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах линейной темпоральной логики LTL. В качестве программных систем, для спецификации поведения которых будет применяться логика LTL, рассматриваются счётчиковые машины Минского. Счётчиковые машины Минского — один из способов формализации интуитивного понятия алгоритма. Они обладают той же вычислительной мощностью, что и машины Тьюринга. Счётчиковая машина имеет вид компьютерной программы, написанной на языке высокого уровня, поскольку содержит переменные, называемые счётчиками, и операторы условного и безусловного перехода, позволяющие строить конструкции циклов. Известно, что любой алгоритм (гипотетически) может быть реализован в виде трёхсчётчиковой машины Минского.

Об авторе

Егор Владимирович Кузьмин
Ярославский государственный университет им. П. Г. Демидова
Россия

Профессор, доктор физико-математических наук

ул. Советская, д. 14, г. Ярославль, 150003



Список литературы

1. E. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.

2. G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.

3. M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.

4. R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.

5. E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.

6. A. Pnueli, “The temporal logic of programs”, in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE Computer Society Press, 1977, pp. 46–57.

7. E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 2001.

8. C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008.

9. Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.

10. E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.

11. E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC Programs”, Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443–451, 2013.

12. E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554–563, 2014.

13. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453–465, 2015.

14. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424–436, 2014.

15. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014.

16. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Automatic Control and Computer Sciences, vol. 50, no. 7, pp. 510–519, 2016.


Для цитирования:


Кузьмин Е.В. LTL-спецификация счётчиковых машин. Моделирование и анализ информационных систем. 2021;28(1):104-119. https://doi.org/10.18255/1818-1015-2021-1-104-119

For citation:


Kuzmin E.V. LTL-Specification of Counter Machines. Modeling and Analysis of Information Systems. 2021;28(1):104-119. (In Russ.) https://doi.org/10.18255/1818-1015-2021-1-104-119

Просмотров: 78


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)