In this section, we describe how temporal logic may be used to fully characterize a reactive module or specify its abstract properties, focusing on a formulation of A/G specifications that we have developed in the past [6, 23] and some of the associated composition rules.
A reactive module is equipped with a set of input/output variables for communication and local variables for storage. Its behaviors are prescribed by an initial condition on the output and local variables and a set of transitions that specify how it may change the values of its output and local variables in one execution step. Additionally, there are fairness conditions that dictate how often each transition should be performed. Semantically, a module is associated with a set of computations or sequences of states, each of which represents a possible ‘open execution’ of the module, i.e., execution of the module together with an arbitrary but compatible environment
that may arbitrarily change the values of its input variables but not its output or local variables.
With temporal logic as the modeling language, we distinguish two kinds of specification: system specification and requirement specification. The system specification of a module gives a full characterization of the module in the sense that the sequences satisfying the specification are exactly those produced from open execution of the module. Assuming a single local variable, its safety part can be put in the form of 2(∃x : 2((first → Init) ∧ N)), where x is the local− variable, Init is a state formula, and N is the disjunction of transition formulae that relate the current values of the variables to their previous values. We omit the formula for fairness. When QPTL is used, values in a finite domain can be encoded by boolean values; for modules with variables of infinite domains, LTL is needed.
Requirement specifications are the usual type of temporal-logic specification, describing abstract properties of a module. A module M is said to satisfy a formula p if every computation of M satisfies p. Let ΦM denote the system specification of M . We will regard ΦM → p as the formal definition of the fact that M satisfies p, denoted as M |= p.
Parallel composition corresponds to conjunction in temporal logic. It follows that, if M is a module of system S (≡ M ∧ M0, for some M0), then M |= p implies S |= p. In other words, every property one deduces (in a modular way) from a particular module will hold for the entire system.
We next review our temporal-logic formulation of A/G specifications. The specification E M of a module, where E is the assumption about its environment and M the guarantee by the module, essentially asserts that M holds at least one step longer than E does, i.e., if the environment has satisfied E up to the previous state then the module will satisfy M up to the current state. If E and M are expressible respectively as 2HE and 2HM, where HE and HM
are past formulae (whose truth depends only on the current and past states), E M (i.e., 2HE 2HM) can be succinctly expressed as 2( ∼2H− E → 2H− M).
Hiding is a common technique for making specifications more abstract and corresponds to existential quantification over flexible variables. A temporal formula ϕ will be written as ϕ(~x) to emphasize that the free (flexible) variables of ϕ are among the tuple ~x of variables. An A/G formula with assumption 2(∃w : 2H− E(x, y, w)) and guarantee 2(∃z : 2H− M(x, y, z)) is defined below; variable x is the input (output) variable of the module (environment) and y the output (input) variable of the module (environment).
2(∃w : 2H− E(x, y, w)) 2(∃z : 2H− M(x, y, z)) =∆ 2[ ∼(∃w : 2H− E(x, y, w)) → (∃z : 2H− M(x, y, z))]
Like in the case without hiding, the defining formula2[ ∼(∃w : 2H− E(x, y, w)) → (∃z : 2H− M(x, y, z))]
says that ∃z : 2H− M(x, y, z) holds at least one step longer than ∃w : 2H− E(x, y, w) does.
The following lemma states that A/G specifications can be composed in a straightforward way:
Lemma 3.1 (Simple Composition) Assuming that w1, . . ., wn, z1, . . ., zn are distinct and
no free variables become bound,
Below is a more general rule for composition.
Theorem 3.2 (Composition) Assuming that w, z, w1, . . ., wn, z1, . . ., zn are distinct and
Intuitively, Premise 1 of the above composition rule says that the assumption about the envi-ronment of a module should follow from the guarantees of other modules and the assumption about the environment of the entire system; while, Premise 2 says that the guarantee of the en-tire system should follow from the guarantees of individual modules and the assumption about its environment.
Our A/G formulation also permits expression of liveness properties in the guarantee part. Typ-ically, they would resemble a Streett acceptance condition.
4 Summary of Research Results
We have obtained two main results from this research; one was planned in the proposal, while the other was not. The planned one states that, for assumption/guarantee formulae in PTL, realizability and hence synthesis are solvable in polynomial space (and therefore in exponential time). This to certain extent achieves our goal of reducing the high complexity of synthesis with arbitrary linear temporal formulae, which is double exponential. The unplanned result is a tool [25], which is still being improved and extended [24], for learning and researching ω-automata and temporal logics. During the course of this research, we came to realize that a deeper understanding of the relation between automata and temporal logic is needed. We developed the tool to facilitate our research. We anticipated that the tool would be useful for other researchers as well; its acceptance to TACAS 2007 was a clear evidence. The tool is freely available on the Web (http://goal.im.ntu.edu.tw/) and now has over 100 registered users.
We next give a bit more details of the main result on synthesis with A/G specifications. To simplify the presentation, we assume the module M shares two variables x and y with its environment E; variable x is the input (output) variable of the module (environment) and y the output (input) variable of the module (environment). Suppose the specification is given in the
form of 2HE(x, y) 2HM(x, y), where HE(x, y) and HM(x, y) are past PTL formulae. Recall that2HE(x, y) 2HM(x, y) can be succinctly expressed as2[ ∼2H− E(x, y) → HM(x, y)]. The formula HM(x, y) in the guarantee part often would be a transition formula that relates the current value of y to the previous value of x, which would make realizability trivially true.
However, HM(x, y) can be more complicated.
We say that 2HM(x, y) constrains E if 2(∃y : 2H− M(x, y)) is not a valid formula, i.e., its truth value depends on the remaining free variable x which is controlled by the environment E;
otherwise, we say 2HM(x, y) does not constrain E.
We claim that, if2HM(x, y) does not constrain E, then realizability of2HE(x, y) 2HM(x, y) is equivalent to satisfiability of the same formula, which is in PSPACE [19].
5 Concluding Remarks (Self Evaluation)
It seems very natural to assume that the specification for a module is given in the A/G style.
We have just touched on a promising direction for synthesis. Efficient algorithms for system construction remain to be developed.
We had planned to exploit the program extraction feature of the Coq [21] proof assistant in this context. However, we were unable to complete this investigation due to rather involved technical difficulties, e.g., the need of a constructive version of temporal logic. We will leave this for future research. We still hope to become the first to successfully use a proof assistant to extract a reactive module from the proof of validity of the implementability formula corresponding to the given specification of the module. For specifications that defy fully algorithmic solutions for synthesis, the machine-assisted approach would provide the only alternative for the automation of open system construction.
This project involved an extensive set of fundamental mathematical and logic tools, including various classes of automata on infinite objects, games, and temporal logic. It helped the par-ticipating students get an early exposure to these foundational tools that should be very useful for their future research careers.
References
[1] M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specification. In Proceedings of the 16th International Colloquium on Automata, Languages, and Programming, LNCS 372, pages 1–17, 1989.
[2] E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999.
[3] E. Gr¨adel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games (LNCS 2500).
Springer, 2002.
[4] C.A.R. Hoare. An axiomatic basis for computer programs. Communications of the ACM, 12(10):576–580, 1969.
[5] C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, October 1983.
[6] B. Jonsson and Y.-K. Tsay. Assumption/guarantee specifications in linear-time temporal logic. Theoretical Computer Science, 167:47–72, October 1996. An extended abstract appeared earlier in TAPSOFT ’95, LNCS 915.
[7] Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and Com-putation, pages 97–109, June 2001.
[8] O. Kupferman and M.Y. Vardi. Synthesizing distributed systems. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pages 389–398, 2001.
[9] L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.
[10] P. Madhusudan and P.S. Thiagarajan. Distributed controller synthesis for local specifica-tions. In Proceedings of the 28th International Colloqium on Automata, Languages, and Programming (ICALP), LNCS 2076, pages 396–407, 2001.
[11] Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings of the 9th ACM Symposium on Principles of Distributed Computing, pages 377–408. ACM, 1990.
[12] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Spec-ification. Springer-Verlag, 1992.
[13] J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417–426, July 1981.
[14] A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179–190, 1989.
[15] A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science (FOCS ’90), pages 746–757, 1990.
[16] S. Schewe and B. Finkbeiner. Bounded synthesis. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), LNCS 4762, pages 474–488, 2007.
[17] S. Schewe and B. Finkbeiner. Distributed synthesis for alternating-time logics. In Pro-ceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), LNCS 4762, pages 268–283, 2007.
[18] A.P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard, 1983.
[19] A.P. Sistla and E.M. Clarke. Complexity of propositional linear temporal logics. Journal of the ACM, 32:733–749, 1985.
[20] A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B¨chi automata with applications to temporal logic. Throretical Computer Science, 49:217–237, 1987.
[21] The Coq Development Team. The Coq Proof Assistant: Reference Manual, 2004.
[22] W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theo-retical Computer Science, Volume B: Formal Models and Semantics, pages 133–191. MIT Press, 1990.
[23] Y.-K. Tsay. Compositional verification in linear-time temporal logic. In J. Tiuryn, editor, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures, LNCS 1784, pages 344–358. Springer, March 2000.
[24] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo. GOAL extended: To-wards a research tool for omega-automata and temporal logic. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). To appear as an LNCS volume.
[25] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. GOAL: A graphical tool for manipulating b¨uchi automata and temporal formulae. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS 4424, pages 466–471. Springer, March 2007.
[26] P. Wolper. Temporal logic can be more expressive. Information and Computation, 56(1-2):72–99, 1983.
Conference Trip Report
11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Braga, Portugal, March 26–30, 2007
(NSC 95-2221-E-002-127dddddddddddd)
Yih-Kuen Tsay ddd
Department of Information Management National Taiwan University
1 Conference Overview
The 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) was held in Braga, Portugal, March 26–30, 2007. TACAS has been one of the five main conferences of the European Joint Conferences on Theory and Practice of Software (ETAPS) since the inception of ETAPS in 1998. ETAPS is now the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS 2007 (March 24–April 1, 2007) also included 16 satellite workshops. The total number of participants was over 450.
TACAS and CAV are probably the two most important conferences on formal verification. The technical program of TACAS 2007 consisted of 2 invited talks and 54 (45 research and 9 tool) papers selected from 204 (170 research and 34 tool) submissions. Apparently, this was a very selective program. The conference proceedings was published as LNCS 4424 of Springer.
One nice thing about a federated conference like ETAPS is that you get many invited talks, one or two for each main conference plus several unifying ones. Below are some highlights. In his TACAS invited talk “There and Back Again: Lessons Learned on the Way to the Market”, Rance Cleaveland from University of Maryland and Fraunhofer USA Center for Experimental Software Engineering and Reactive Systems Inc. talked about his experience in commercializing his research results and tools. As he contended, one should always try to package a tool in a way that suits the user’s daily practice. In another TACAS invited talk “Verifying Object-Oriented Software: Lessons and Challenges”, K. Rustan M. Leino from Microsoft Research, Redmond, USA introduced the Spec# system. He also did a demo of the system. In a unifying invited talk “Contract-Driven Development”, Bertrand Meyer from ETH Z¨urich, Switzerland reflected on the development of the Eiffel approach and tool. Eiffel had just won the prestigious
ACM Software System Award (former winners include UNIX, TeX, TCP/IP, SMALLTALK, WWW, Tcl/Tk, Java, etc.). Meyer jokingly dubbed the Spec# system as Eiffel in braces.
Aspect-oriented programming has emerged as a new paradigm in the design and development of software systems. In his FOSSACS invited talk “Formal Foundations for Aspects”, Radha Jagadeesan from DePaul University, USA argued that aspects are no more intractable than stateful higher order programs.
2 Presentation of My Paper
I presented the following paper which I co-authored with four of my students:
Title: GOAL: A Graphical Tool for Manipulating B¨uchi Automata and Temporal Formulae Authors: Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu and Wen-Chin Chan The paper describes a tool, named GOAL, that we have been developing for learning and researching omega-automata and linear temporal logics. The tool had earlier been introduced in an informal workshop FMEd affiliated with FM 2006. My Ph.D. student Yu-Fang Chen also attended the conference. To allow him to gain some experience and to get exposed, I asked him to do the demo part of the 30-minute presentation.
Our tool was well received by the participants. Several of them came to greet us right after our presentation. One of them even suggested an efficient procedure, though not difficult to conceive, for testing the equivalence between a B¨uchi automaton and a temporal formula. The equivalence test was not directly supported by our tool at that time. His suggestion prompted us to implement it in the next version.
3 Meeting Old Friends
I met Parosh Abdulla, a former colleague at Uppsala University back in 1993-5 while I was a postdoctoral researcher there. We had worked together with ˇCer¯ans and Jonsson to develop fundamental theorems for the verification of infinite-state systems. Our joint work turned to be an influential one, accumulating a considerable number of citations over the years. Abdulla is still very actively pursuing various directions of the same research topic. Through Abdulla, I also got to know Ahmed Bouajjanni from Paris 7 during the conference. Bouajjanni is also very active in the same area and a frequent co-author of Abdulla.
I was also very happy to meet for the third time Ridha Khedri. He visited Taipei for the ATVA conference in 2003. I met him again in FM 2006, of which his institute was the host, just a few months prior to TACAS. Khedri has been a faculty member at McMaster University, Canada for some time. He is an expert in algebras and their applications. It is always very nice to have someone showing you things, technical or non-technical, from a different perspective. We had a dinner and a few walks around the host town. Khedri originally was from Tunisia and from his story telling I realized how little I knew about North Africa.
Finally, I must mention Moshe Vardi, who is considered by many father of the automata-theoretical approach to model checking. Vardi visited Taipei for the ATVA conference in 2004 and subsequently helped me to get the proceedings of ATVA 2005 (of which I was PC co-chair) published in the LNCS series of Springer. He seemed to be very interested in the GOAL tool that I presented and pointed out a noteworthy B¨uchi complementation algorithm by him, Kupferman, and two other authors. The algorithm has now been implemented in GOAL.