LTL-specification for development and verification of control programs

Autor: Maxim V. Neyzov, Egor V. Kuzmin

Publikováno v: Моделирование и анализ информационных систем, Vol 30, Iss 4, Pp 308-339 (2023)

This work continues the series of articles on development and verification of control programs based on the LTL-specification. The essence of the approach is to describe the behavior of programs using formulas of linear temporal logic LTL of a specia

Externí odkaz: https://doaj.org/article/584203ca53f54d858b748005cf82c3de

On Families of Full Trios Containing Counter Machine Languages

Autor: Oscar H. Ibarra, Ian McQuillan

We look at nondeterministic finite automata augmented with multiple reversal-bounded counters where, during an accepting computation, the behavior of the counters is specified by some fixed pattern. These patterns can serve as a useful "bridge" to ot

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d7b4837c969a0a6ff65ba8cf3ba39e13
http://arxiv.org/abs/2212.03791

On languages of automaton counter machines

Autor: E. V. Kuzmin, D. Ju. Chalyy

Publikováno v: Моделирование и анализ информационных систем, Vol 17, Iss 2, Pp 48-71 (2010)

Some properties of formal languages (ACML) of automaton counter machines are investigated. We show that a class of these languages is closed with respect to the following operations: union, intersection by regular sets, concatenation, infinite iterat

Externí odkaz: https://doaj.org/article/fe76d43605ea4b23865a1623ed2b8b25

On a reachability set of automaton 3-counter machines

Autor: E. V. Kuzmin, D. J. Chalyy

Publikováno v: Моделирование и анализ информационных систем, Vol 16, Iss 3, Pp 77-84 (2009)

In this paper we prove the existence of automaton 3-counter machines which have non-semilinear reachability sets.

Externí odkaz: https://doaj.org/article/bffe0971efbb469aa292697fd4834739

Reachability for Two-Counter Machines with One Test and One Reset

Autor: Finkel, Alain, Leroux, Jérôme, Sutre, Grégoire

Publikováno v: FSTTCS 2018-38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
FSTTCS 2018-38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2018, Ahmedabad, India. pp.31:1-31:14, ⟨10.4230/LIPIcs.FSTTCS.2018.31⟩

International audience; We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::55d8935032fb82dc036dcda1f7268cbc
https://hal.archives-ouvertes.fr/hal-01848554