Z. Manna
A. Pnueli
ABSTRACT
∀-automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a ∀-automaton.
- K. Apt, G.D. Plotkin -- Countable Nondeterminism and Random Assignment, JACM 33, 4 (1986), 724-767. Google Scholar
Digital Library
- B. Alpern, F.B. Schneider -- Verifying Temporal Properties without using Temporal Logic, Technical Report TR 85-723, Cornell University (December 1985).Google Scholar
- E.M. Clarke, E.A. Emerson, A.P. Sistla -- Automatic Verification of Finite-State Concurrent Systems using Temporal Logic specifications, TOPLS 8, 2 (april 1986), 244-263. Google ScholarDigital Library
- E.W. Dijkstra -- A Discipline of Programming, Prentice Hall (1976). Google ScholarDigital Library
- E.A. Emerson, C.L. Lei -- Modalities for Model Checking: Branching Time Strikes Back, 12th Symp. on Principles of Programming Languages (1985), 84-96. Google ScholarDigital Library
- R.W. Floyd -- Assigning Meanings to Programs, in Mathematical Aspects of Computer Science, 19th Symp. of Appl. Math., American Mathematical Society, Providence (1967), 19-32.Google Scholar
- N. Francez -- Fairness, Springer-Verlag (1986).Google Scholar
- O. Grumberg, N. Francez, J.A. Makowsky, W.P. deRoever -- A Proof Rule for Fair Termination of Guarded Commands, Information and Control 66 (1985), 83- 102. Google ScholarDigital Library
- D. Harel -- Statecharts: A Visual Formalism for Complex Systems, Technical Report, Weizmann Institute (1984).Google Scholar
- D. Harel -- Effective Transformations on Infinite Trees, with Applications to High Undecidability, Dominoes, and Fairness, JACM 33, 1 (1986), 224-248. Google ScholarDigital Library
- C.A.R. Hoare -- An Axiomatic Approach to Computer Programming, CACM 12 (1969), 576-583. Google ScholarDigital Library
- O. Lichtenstein, A. Pnueli -- Checking that Finite-State Concurrent Programs Satisfy their Linear Specifications, 12th Symp. on Principles of Programming Languages (1985), 97-107. Google ScholarDigital Library
- D. Lehmann, A. Pnueli, J. Stavi -- Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, LNCS 115, Springer-Verlag (1981). Google ScholarDigital Library
- Z. Manna, A. Pnueli -- The Temporal Framework for Concurrent Programming, in The Correctness Problem in Computer Science (R.S. Boyer, J.S. Moore, eds.), Academic Press (1981), 215-274.Google Scholar
- Z. Manna, A. Pnueli -- Adequate Proof Principles for Invariances and Liveness Properties of Concurrent Programs, Science of Computer Programming 4 (1984), 257-289. Google ScholarDigital Library
- Z. Manna, A. Pnueli -- Specification and Verification of Concurrent Programs by ¿-Automata, Computer Science Report, Stanford University (January 1987).Google Scholar
- S. Owicki, L. Lamport -- Proving Liveness Properties of Concurrent Programs, TOPLAS 4, 3 (1982), 455-495. Google ScholarDigital Library
- G.L. Peterson -- Myths about the Mutual-exclusion Problem, Information Processing Letters 12, 3 (1981), 115-116.Google ScholarCross Ref
- F.A. Stomp, W.P. deRoever, R.T. Gerth -- The μ-Calculus as an Assertion Language for Fairness Arguments, Technical Report 84-12, Utrecht (1984).Google Scholar
- M.Y. Vardi, P. Wolper -- An Automata-theoretic Approach to Automatic Program Verification, IEEE Symp. on Logic in Computer Science, Cambridge (1986), 332- 344.Google Scholar
- P. Wolper -- Temporal Logic can be More Expressive, 22nd Symp. on Foundations of Computer Science (1981), 340-348. Google ScholarDigital Library
- P. Wolper, M.Y. Vardi, A.P. Sistla -- Reasoning about Infinite Computation Paths, 24th IEEE Symp. on Foundations of Computer Science, Tucson (1983), 185-194. Google ScholarDigital Library
Index Terms
- Specification and verification of concurrent programs by A ∀ automata
Recommendations
Past pushdown timed automata and safety verification
Implementation and application automataWe consider past pushdown timed automata that are discrete pushdown timed automata with past formulas as enabling conditions. Using past formulas allows a past pushdown timed automaton to access the past values of the finite state variables in the ...
Presburger liveness verification of discrete timed automata
Using an automata-theoretic approach, we investigate the decidability of liveness properties (called Presburger liveness properties) for timed automata when Presburger formulas on configurations are allowed. While the general problem of checking a ...
Comments