Verification of concurrent programs: The automata-theoretic framework.

*(English)*Zbl 0725.03013An effective version of Wolper’s temporal logic IPTL, recursive infinitary temporal logic (RITL) is introduced, and it is proved that the properties expressed in RITL can be captured by recursive automata on infinite trees. Three types of acceptance conditions (Wolper acceptance, Büchi acceptance, and Streett acceptance) for these automata are considered and shown to be of the same power. This enables to define effective equivalent transformations of recursive trees with complicated correctness conditions to trees with simpler ones (nondeterministic programs are naturally associated to their computational trees, which are recursive).

This transformation technique is then applied to verification of concurrent and nondeterministic programs. Proof methods for two approaches to fair termination are developed: the method of explicit schedulers, and the method of helpful directions. The idea is that, given a computation tree of a program and a correctness condition, both defined via recursive automata, one constructs new automata which terminate iff the program is correct. If, for example, the correctness is formulated in RITL, we can express it in terms of recursive automata. Hence correctness is reduced to termination.

This transformation technique is then applied to verification of concurrent and nondeterministic programs. Proof methods for two approaches to fair termination are developed: the method of explicit schedulers, and the method of helpful directions. The idea is that, given a computation tree of a program and a correctness condition, both defined via recursive automata, one constructs new automata which terminate iff the program is correct. If, for example, the correctness is formulated in RITL, we can express it in terms of recursive automata. Hence correctness is reduced to termination.

Reviewer: A.P.Stolboushkin (Pereslavl-Zalessky)

##### MSC:

03B70 | Logic in computer science |

03D05 | Automata and formal grammars in connection with logical questions |

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

##### Keywords:

recursive infinitary temporal logic; recursive automata on infinite trees; acceptance conditions; correctness; verification of concurrent and nondeterministic programs; termination
PDF
BibTeX
Cite

\textit{M. Y. Vardi}, Ann. Pure Appl. Logic 51, No. 1--2, 79--98 (1991; Zbl 0725.03013)

Full Text:
DOI

##### References:

[1] | Alpern, B.; Schneider, F.B., Verifying temporal properties without using temporal logic, ACM trans. programming languages, 11, 147-167, (1989) · Zbl 0676.68003 |

[2] | Alpern, B.; Schneider, F.B., Proving Boolean combinations of deterministic properties, Proc. 2nd IEEE symp. on logic in computer science, 131-137, (1987), Ithaca |

[3] | Apt, K.R., Ten years of Hoare’s logic: a survey—part I, ACM trans. programming languages and systems, 3, 431-483, (1981) · Zbl 0471.68006 |

[4] | Apt, K.R., Ten years of Hoare’s logic: a survey—part II, Theoret. comput. sci., 28, 83-109, (1984) · Zbl 0523.68015 |

[5] | Apt, K.R.; Olderog, E.R., Proof rules and transformation dealing with fairness, Sci. comput. programming, 3, 65-100, (1983) · Zbl 0512.68014 |

[6] | Apt, K.R.; Plotkin, G.D., Countable nondeterminism and random assignment, J. assoc. comput. Mach., 33, 724-767, (1986) · Zbl 0627.68015 |

[7] | Apt, K.R.; Pnueli, A.; Stavi, J., Fair termination revisited—with delay, Theoret. comput. sci., 33, 65-84, (1984) · Zbl 0542.68015 |

[8] | Boom, H.J., A weaker precondition for loops, ACM trans. programming languages and systems, 4, 668-677, (1982) · Zbl 0492.68014 |

[9] | Büchi, J.R., On a decision method in restricted second-order arithmetics, (), 1-12 · Zbl 0147.25103 |

[10] | Choueka, Y., Theories of automata on ω-tapes—a simplified approach, J. comput. system sci., 8, 117-141, (1974) · Zbl 0292.02033 |

[11] | Clarke, E.M.; Emerson, E.A.; Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specification, ACM trans. programming languages and systems, 8, 244-263, (1986) · Zbl 0591.68027 |

[12] | Dayan, I.; Harel, D., Fair termination with cruel schedulers, Fund. inform., 9, 1-12, (1986) · Zbl 0598.68026 |

[13] | Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013 |

[14] | Francez, N., Fairness, Texts monographs comput. sci., (1986), Springer New York · Zbl 0602.68007 |

[15] | Grumberg, O.; Francez, N.; Makowsky, J.A.; de Roever, W.P., A proof rule for fair termination of guarded command, Inform. and control, 66, 83-102, (1985) · Zbl 0577.68022 |

[16] | Hailpern, B.T.; Owicki, S.S., Modular verification of computer communication protocols, IEEE trans. comm., 31, 56-68, (1983) |

[17] | Harel, D., Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness, J. assoc. comput. Mach., 33, 225-248, (1986) |

[18] | Harel, D.; Pnueli, A.; Stavi, J., Propositional dynamic logic of nonregular programs, J. comput. system sci., 26, 222-243, (1983) · Zbl 0536.68041 |

[19] | Lehman, D.; Pnueli, A.; Stavi, J., Impartiality, justice, and fairness—the ethic of concurrent termination, (), 264-277 |

[20] | Lichtenstein, O.; Pnueli, A., Checking that finite-state concurrent programs satisfy their linear specification, Proc. 12th ACM symp. on principles of programming languages, 97-107, (1985) |

[21] | Manna, Z.; Pnueli, A., Verification of concurrent programs: the temporal framework, in: the correctness problem in computer science, (), 215-273 |

[22] | Manna, Z.; Pnueli, A., How to cook a temporal proof system for your pet language, Proc. 10th symp. on principles of programming languages, 141-154, (1983), Austin, TX |

[23] | Manna, Z.; Pnueli, A., Proving precedence properties: the temporal way, (), 491-512 |

[24] | Manna, Z.; Pnueli, A., Adequate proof principles for invariance and liveness of concurrent programs, Sci. comput. programming, 4, 257-289, (1984) · Zbl 0542.68014 |

[25] | Manna, Z.; Pnueli, A., Specification and verification of concurrent programs by ∀-automata, (), 1-12, Munich |

[26] | Nivat, M., Behaviors of processes and synchronized systems, (), 473-550 |

[27] | Owicki, S.S.; Lamport, L., Proving liveness properties of concurrent programs, ACM trans. programming languages and systems, 4, 455-495, (1982) · Zbl 0483.68013 |

[28] | Park, D., On the semantics of fair parallelism, Proc. Copenhagen winter school on abstract software specification, 86, (1979), Springer New York, Lecture Notes in Comput. Sci. |

[29] | Park, D., A predicate transformer for weak fair termination, Proc. 6th IBM symp. on math. foundations of computer science, (1981), Hakone, Japan |

[30] | Park, D., Concurrency and automata on infinite sequences, (), 167-183, Lecture Notes in Comput. Sci. |

[31] | Pnueli, A., The temporal logic of programs, Proc. 18th symp. on foundations of computer science, 46-57, (1977) |

[32] | Pnueli, A., The temporal semantics of concurrent programs, Theoret. comput. sci., 13, 45-60, (1981) · Zbl 0441.68010 |

[33] | Queille, J.P.; Sifakis, J., Fairness and related properties in transition systems—a temporal logic to deal with fairness, Acta inform., 19, 195-220, (1983) · Zbl 0489.68024 |

[34] | Rescher, N.; Urquhart, A., Temporal logic, (1971), Springer New York · Zbl 0229.02027 |

[35] | Rinat, R.; Francez, N.; Grumberg, O., Infinite trees, markings, and well-foundedness, Inform. and comput., 79, 131-154, (1988) · Zbl 0659.68021 |

[36] | Rogers, H., Theory of recursive functions and effective computability, (1967), McGraw-Hill New York · Zbl 0183.01401 |

[37] | Sistla, A.P., Fairness, marked trees, and automata, (1986), Unpublished manuscript |

[38] | Sistla, A.P., On verifying that a concurrent program satisfies a non-deterministic specification, Technical report TR 88-378.01.1, (1988), GTE Laboratories · Zbl 0677.68011 |

[39] | Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logics, J. assoc. comput. Mach., 32, 733-749, (1985) · Zbl 0632.68034 |

[40] | Sistla, A.P.; Vardi, M.Y.; Wolper, P., The complementation problem for Büchi automata with applications to temporal logic, Theoret. comput. sci., 49, 217-237, (1987) · Zbl 0613.03015 |

[41] | Streett, R.S., Propositional dynamic logic of looping and converse, Inform. and control, 54, 121-141, (1982) · Zbl 0515.68062 |

[42] | Vardi, M.Y., Automatic verification of probabilistic concurrent finite-state programs, Proc. 26th IEEE symp. on foundations of computer science, 327-338, (1985), Portland |

[43] | Vardi, M.Y.; Wolper, P., An automata-theoretic approach to automatic program verification, Proc. IEEE symp. on logic in computer science, 332-344, (1986), Cambridge |

[44] | Vardi, M.Y.; Wolper, P., Reasoning about infinite computation paths, IBM research report RJ6209, (1988) |

[45] | Wagner, K.; Staiger, L., Recursive ω-languages, (), 532-537 · Zbl 0367.02017 |

[46] | Wolper, P., Temporal logic can be more expressive, Inform. and control, 56, 72-99, (1983) · Zbl 0534.03009 |

[47] | Wolper, P., Expressing interesting properties of programs in propositional temporal logic, Proc. 13th ACM symp. on principles of programming languages, 184-193, (1986), St. Petersburg Beach, FL |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.