Compositional Synthesis of Generalized Mealy Machines

• Autorzy: Tini S. , Maggiolo-Schettini A.
• Języki publikacji: EN

Abstrakty

EN

We give an algorithm for synthesizing Generalized Mealy Machines from LTL-formulae. The main novelty of the paper is that the algorithm is compositional. Its complexity coincides with the lower bound of the synthesis problem.

Słowa kluczowe

EN

Mealy machine; LTL; synthesis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 367--382
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Tini S.

• Dipartimento di Scienze della Cultura, Politiche e dell'Informazione, Universita dell'Insubria, Via Valleggio 11, 22100 Como, Italy

autor

Maggiolo-Schettini A.

• Dipartimento di Informático, Universitá di Pisa, Via Buonarroti 2, 56127 Pisa. Italy

Bibliografia

• [1] M. Abadi. L. Lamport, and P. Wolper, Realizable and Unrealizable Specifications of Reactive Systems. In Proc. Intern. Coll. on Automata. Languages and Programming, Lecture Notes in Computer Science 372, Springer, Berlin, 1989, 1-17.
• [2] A. Arora, PC. Attie, and E.A. Emerson, Synthesis of Fault-tolerant Concurrent Programs. In Proc. ACM Symp. on Principles of Distributed Computing, ACM Press, 1998, 173-182.
• [3] P.C. Attie and E.A. Emerson, Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation. In Proc. ACM Symp. on Principles of Distributed Computing, ACM Press, 1996, 111-120.
• [4] A. Benveniste and G. Berry (Eds.), Another Look ¿it Real-time Systems. Proc. IEEE 79, 1991, 1268-1336.
• [5] E.A. Emerson, Temporal and Modal Logic. In J. van Leeuwen Ed., Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics. Elsevier and The MIT Press, 1990, 995-1072.
• [6] E.A. Emerson and E.M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Programming 2, 1982, 241-266.
• [7] D. Harel and A. Pnueli. On the Development of Reactive Systems. In K.R. Apt Ed. Logic and Models of Concurrent Systems, NATO, ASI-13, Springer, New York. 1985.477-498.
• [8] Z. Manna and P. Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 6. 1984, 68-93.
• [9] A. Pnueli and R. Rosner, On the Synthesis of a Reactive Module. In Proc. ACM Symp. on Principles of Programming Languages, ACM Press, 1989, 179-191.
• [10] A. Pnueli and R. Rosner, On the Synthesis of an Asynchronous Reactive Module. In. Proc. Intern. Coll. On Automata, Languages and Programming, Lecture Notes in Computer Science 372, Springer, Berlin, 1989, 652-671.
• [11] R. Rosner, Modular Synthesis of Reactive Systems. Ph.D. Thesis. Weizmann Institute of Science, 1992.
• [12] P. Wolper, Constructing Automata From Temporal Logic Formulas: A Tutorial. In E. Brinksma, H. Hermanns, and J.P Katoen Eds., Lectures on Formal Methods and Performance Analysis, Lecture Notes in Computer Science 2090, Springer, Berlin, 2000, 261-277.