Advertisement

Synthesis of Trigger Properties

  • Orna Kupferman
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)

Abstract

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for temporal synthesis, little of this theory has been reduced to practice. This is in contrast with model-checking theory, which has led to industrial development and use of formal verification tools. We address this problem here by considering a certain class of PSL properties; this class covers most of the properties used in practice by system designers. We refer to this class as the class of trigger properties.

We show that the synthesis problem for trigger properties is more amenable to implementation than that of general PSL properties. While the problem is still 2EXPTIME-complete, it can be solved using techniques that are significantly simpler than the techniques used in general temporal synthesis. Not only can we avoid the use of Safra’s determinization, but we can also avoid the use of progress ranks. Rather, the techniques used are based on classical subset constructions. This makes our approach amenable also to symbolic implementation, as well as an incremental implementation, in which the specification evolves over time.

Keywords

Regular Expression Synthesis Problem Atomic Proposition Acceptance Condition Tree Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. AFF+02.
    Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 196–211. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. ALW89.
    Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  3. AMPS98.
    Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symposium on System Structure and Control, pp. 469–474. Elsevier, Amsterdam (1998)Google Scholar
  4. AT04.
    Alur, R., La Torre, S.: Deterministic generators and games for ltl fragments. ACM Transactions on Computational Logic 5(1), 1–25 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  5. STW05.
    Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of Büchi automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 262–272. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. BBEF+01.
    Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. BDF+04.
    Basin, D.A., Deville, Y., Flener, P., Hamfelt, A., Nilsson, J.F.: Synthesis of programs in computational logic. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 30–65. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. BFG+05.
    Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. BGJ+07.
    Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: Proc. Conference on Design, Automation and Test in Europe, pp. 1188–1193. ACM, New York (2007)Google Scholar
  10. BL69.
    Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  11. CGP99.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  12. Cho74.
    Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of Computer and Systems Science 8, 117–141 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  13. Chu63.
    Church, A.: Logic, arithmetics, and automata. In: Proc. Int. Congress of Mathematicians, 1962, pp. 23–35. Institut Mittag-Leffler (1963)Google Scholar
  14. CKS81.
    Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association for Computing Machinery 28(1), 114–133 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  15. Dil89.
    Dill, D.L.: Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, Cambridge (1989)Google Scholar
  16. DR09.
    Doyen, L., Raskin, J.-F.: Antichains for the automata-based approach to model-checking. Logical Methods in Computer Science 5(1) (2009)Google Scholar
  17. EC82.
    Emerson, E.A., Clarke, E.M.: Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)CrossRefzbMATHGoogle Scholar
  18. EF06.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)Google Scholar
  19. EKM98.
    Elgaard, J., Klarlund, N., Möller, A.: Mona 1.x: new techniques for WS1S and WS2S. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  20. EL86.
    Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 267–278 (1986)Google Scholar
  21. HRS05.
    Harding, A., Ryan, M., Schobbens, P.: A new algorithm for strategy synthesis in LTL games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 477–492. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  22. HU79.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  23. Jur00.
    Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. Kla98.
    Klarlund, N.: Mona & Fido: The logic-automaton connection in practice. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414. Springer, Heidelberg (1998)Google Scholar
  25. KPV06.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  26. KV98c.
    Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: from linear-time to branching-time. In: Proc. 13th IEEE Symp. on Logic in Computer Science, pp. 81–92 (1998)Google Scholar
  27. KV98b.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Proc. 30th ACM Symp. on Theory of Computing, pp. 224–233 (1998)Google Scholar
  28. KV00a.
    Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109–127. Kluwer Academic Publishers, Dordrecht (2000)CrossRefGoogle Scholar
  29. KV05a.
    Kupferman, O., Vardi, M.Y.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 206–221. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  30. KV05b.
    Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM Transactions on Computational Logic 6(2), 273–294 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  31. KV05c.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)Google Scholar
  32. LP85.
    Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 97–107 (1985)Google Scholar
  33. MH84.
    Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  34. MS08.
    Morgenstern, A., Schneider, K.: From ltl to symbolically represented deterministic automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 279–293. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  35. MS08b.
    Morgenstern, A., Schneider, K.: Generating deterministic ω-automata for most LTL formulas by the breakpoint construction. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Freiburg, Germany (2008)Google Scholar
  36. MW80.
    Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Transactions on Programming Languagues and Systems 2(1), 90–121 (1980)CrossRefzbMATHGoogle Scholar
  37. MW84.
    Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languagues and Systems 6(1), 68–93 (1984)CrossRefzbMATHGoogle Scholar
  38. Pit07.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3), 5 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  39. Pnu77.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46–57 (1977)Google Scholar
  40. PPS06.
    Piterman, N., Pnueli, A., Saar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  41. PR89a.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179–190 (1989)Google Scholar
  42. PR89b.
    Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  43. Rab72.
    Rabin, M.O.: Automata on infinite objects and Church’s problem. Amer. Mathematical Society, Providence (1972)CrossRefzbMATHGoogle Scholar
  44. Ros92.
    Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)Google Scholar
  45. RS59.
    Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)MathSciNetCrossRefzbMATHGoogle Scholar
  46. SDC01.
    Shimizu, K., Dill, D.L., Chou, C.-T.: A specification methodology by a collection of compact properties as applied to the intel itanium processor bus protocol. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 340–354. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  47. THB95.
    Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261–277. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  48. TV07.
    Tabakov, D., Vardi, M.Y.: Model checking Büechi specifications. In: 1st International Conference on Language and Automata Theory and Application Principles of Programming Languages (2007)Google Scholar
  49. Var95c.
    Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 267–292. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  50. VR05.
    Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)Google Scholar
  51. VS85.
    Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: Proc. 17th ACM Symp. on Theory of Computing, pp. 240–251 (1985)Google Scholar
  52. VW86a.
    Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer and Systems Science 32(2), 182–221 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  53. VW94.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  54. WD90.
    Wong-Toi, H., Dill, D.L.: Synthesizing processes and schedulers from temporal specifications. In: Clarke, E.M., Kurshan, R.P. (eds.) Proc. 2nd Int. Conf. on Computer Aided Verification. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 177–186. AMS, Providence (1991)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Orna Kupferman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.School of Engineering and Computer ScienceHebrew UniversityJerusalemIsrael
  2. 2.Department of Computer ScienceRice UniversityHoustonU.S.A.

Personalised recommendations