Abstract
For two fragments LP and LF of monadic first-order logic with bounded quantifiers, the corresponding versions of the proposed specification theorem are formulated and proved that allow one to reduce the procedure for synthesizing Σ-automata specified by formulas of these logics to an equivalent transformation of formulas.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
M. Abadi, L. Lamport, and P. Wolper, “Realizable and unrealizable specifications of reactive systems,” in: Lecture Notes in Computer Science, Vol. 372, Springer, Berlin-Heidelberg (1989), pp. 1–17.
A. Pnueli and R. Rosner, “On the synthesis of a reactive module,” in: Proc. 16th ACM Symp. on Principles of Programming Languages, Austin (1989), pp. 179–190.
R. Alur and S. La Torre, “Deterministic generators and games for LTL fragments,” ACM Transactions on Computational Logic, Vol. 5, No 1, 1–25 (2004).
A. Harding, M. Ryan, and P.-J. Schobbens, “A new algorithm for strategy synthesis in LTL games,” in: Lecture Notes in Computer Science, Vol. 3440, Springer, Berlin-Heidelberg (2005), pp. 477–492.
N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of reactive(1) designs” in: Lecture Notes in Computer Science, Vol. 3855, Springer, Berlin-Heidelberg (2006), pp. 364–380.
A. N. Chebotarev, “Harmonization of automata specifications represented in the language L,” Cybernetics and Systems Analysis, Vol. 52, No. 3, 341–350 (2016).
B. Alpern and F. Schneider, “Recognizing safety and liveness,” Distributed Computing, No. 2, 117–126 (1987).
A. N. Chebotarev, “Harmonization of interacting automata,” Cybernetics and Systems Analysis, Vol. 51, No. 5, 676–686 (2015).
A. N. Chebotarev, “Regular form of deterministic FSMs specification in the language L,” Applied Discrete Mathematics, No. 4, 64–72 (2010).
A. N. Chebotarev, “Extension of the automaton specification logical language and the synthesis problem,” Cybernetics and Systems Analysis, Vol. 32, No. 6, 756-765 (1996).
A. N. Chebotarev, “Synthesis of a procedural representation of an automaton specified in the logical language L*. I,” Cybernetics and Systems Analysis, Vol. 33, No. 4, 505–515 (1997).
A. N. Chebotarev, “Some subsets of monadic first-order logic (MFO) used for the specification and synthesis of Σ-automata,” Cybernetics and Systems Analysis, Vol. 53, No. 4, 512–523 (2017).
O. Finkel, “Topological properties of omega context free languages,” Theoretical Computer Science, Vol. 262 (1–2), 669–697 (2001).
Author information
Authors and Affiliations
Corresponding author
Additional information
Translated from Kibernetika i Sistemnyi Analiz, No. 5, September–October, 2017, pp. 22–33.
Rights and permissions
About this article
Cite this article
Chebotarev, A.N. Problems of Synthesis of Σ-Automata Specified in Languages LP and LF of First Order Logic. Cybern Syst Anal 53, 675–683 (2017). https://doi.org/10.1007/s10559-017-9969-8
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10559-017-9969-8