Skip to main content
SpringerLink
Log in

Automated deduction of finite-state control programs for reactive systems

  • Conference paper
  • First Online:
Automated Deduction — CADE-15 (CADE 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1421))

Included in the following conference series:

  • 128 Accesses

Abstract

We propose an approach towards the automatic synthesis of finite-state reactive control programs from purely declarative, logic specifications of their requirements. More precisely, if P is a set of propositional temporal logic formulas, representing the environment of a reactive system, and if a is a propositional formula, representing a safety requirement, then we point out how to deduce a most general set C of formulas, representing a control program, such that P ∪ C ≒ α.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Burch, J. R., Clarke, E. M., McMillan, K. L.: Symbolic model checking: 1020 states and beyond. Information and Computing 98 (2), 142–170, 1992.

    Article  MathSciNet  Google Scholar 

  2. Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. E., Dill, D. L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and systems 13 (4), 1994.

    Google Scholar 

  3. Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79 (9), 1270–1282, 1991.

    Article  Google Scholar 

  4. Balemi, S., Hoffmann, G. J., Gyugyi, P., Wong-Toi, H., Franklin, G. F.: Supervisory control of a rapid thermal multiprocessor. IEEE Transactions on Automatic Control 38 (7), 1040–1059, 1993.

    Article  MathSciNet  Google Scholar 

  5. Bryant, R. E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp. 35 (8), 677–691, 1986.

    MATH  Google Scholar 

  6. Clarke, E. M., Emerson, E. A., Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8 (2), 244–263, 1986.

    Article  Google Scholar 

  7. Dutertre, B., Le Borgne, M.: Control of polynomial dynamical systems: an example. Tech. Report 2193, INRIA, 1994.

    Google Scholar 

  8. Emerson, E. A., Clarke, E. M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266, 1982.

    Article  Google Scholar 

  9. Fisher, M.: A normal form for first-order temporal formulae. Proc. 9th International Conference in Automated Deduction, CADE-9, 371–384, Springer, 1992.

    Google Scholar 

  10. Fisher, M., Owens, R.: An introduction to executable modal and temporal logics. Proc. IJCAI Workshop on Executable Modal and Temporal Logics, 1–20, Springer, 1993.

    Google Scholar 

  11. Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer, 1993.

    Google Scholar 

  12. Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems, ed. K. R. Apt, NATO ASI Series, vol. 13, 477–498, Springer, 1985.

    Google Scholar 

  13. Lloyd, J. W.: Foundations of Logic Programming. Springer, 1984.

    Google Scholar 

  14. Malik, R., Mayer, O.: Eine Fixpunkt-Semantik für temporal stratifizierte Programme. Interner Bericht, FB Informatik, UniversitÄt Kaiserslautern, 1994.

    Google Scholar 

  15. Malik, R.: Automatische Synthese diskreter Steuerungen aus logischen Spezifikationen. Shaker Verlag, Aachen, 1998; also available as: Dissertation, FB Informatik, UniversitÄt Kaiserslautern, 1997.

    Google Scholar 

  16. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems — Specification. Springer 1992.

    Google Scholar 

  17. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems — Safety. Springer, 1995.

    Google Scholar 

  18. Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. Proc. Logics of Programs, 253–281, 1981.

    Google Scholar 

  19. McMillan, K. L.: Symbolic Model Checking. Kluwer, 1993.

    Google Scholar 

  20. Ostroff, J.: Temporal logic for real-time systems. Research Studies Press Ltd., Advanced Software Development Series, Taunton, Somerset, 1989.

    Google Scholar 

  21. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. Proc. 16th ACM Symp. on Principles of Programming Languages POPL '89, 1989.

    Google Scholar 

  22. Ramadge, P. J. G., Wonham, W. M.: The control of discrete event systems. Proc. IEEE 77 (1), 81–98, 1989.

    Article  Google Scholar 

  23. Ratel, C., Halbwachs, N., Raymond, P.: Programming and verifying critical systems by means of the synchronous data-flow language Lustre. Software Engineering Notes 16 (5), 112–119, 1991.

    Article  Google Scholar 

  24. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309, 1955.

    MATH  MathSciNet  Google Scholar 

  25. Wonham, W. M., Ramadge, P. J.: On the supremal controllable sublanguage of a given language. SIAM J. Control and Optimization 25 (3), 637–650, 1987.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Kaiserslautern, P.O. Box 3049, 67653, Kaiserslautern, Germany

    Robi Malik

Authors
  1. Robi Malik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Malik, R. (1998). Automated deduction of finite-state control programs for reactive systems. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054268

Download citation

  • DOI: https://doi.org/10.1007/BFb0054268

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

  • Online ISBN: 978-3-540-69110-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation