×

Time and logic: a computational approach. (English) Zbl 0849.03011

London: UCL Press. viii, 325 p. (1995).
This book contains a collection of seven articles on temporal logic and formal methods of temporal reasoning. The first chapter, “Temporal logic of programs: standard approach” by A. Szałas (pp. 1-50), surveys fundamental aspects of propositional and first-order predicate temporal logics, discusses methodological properties of several proof systems for proving time-dependent properties, and investigates their soundness and completeness. The formal specification of algorithms and data structures by means of temporal logics is also discussed. The following chapter, “Effective temporal logics of programs” by H. Andréka, V. Goranko, S. Mikulás, I. Németi and I. Sain (pp. 51-129), gives a comprehensive study and comparison of effective proof systems for propositional and first-order temporal logics of programs. In the third chapter, “On the relation of programs and computations to models of temporal logics” (pp. 131-178), P. Wolper uses techniques of automata theory for the formal verification of temporal properties of programs. Various temporal program verification methods are treated, deterministic and nondeterministic programs are studied, and linear time, branching time and partially ordered time structures are considered. The fourth chapter, “Branching time and partial order in temporal logics” by W. Penczek (pp. 179-228), surveys propositional temporal logics with branching time and partially ordered time. Those logics are motivated by semantical considerations of modeling the behavior of concurrent programs that go beyond interleaving models. Various proof systems are presented and completeness, decidability, model checking and expressiveness issues of temporal logics are discussed. The fifth chapter, “Temporal logic in a stochastic environment” by B. Strulo, D. Gabbay and P. G. Harrison (pp. 229-247), describes a new approach to modelling a temporal logic system in a random environment. The underlying model is based on stochastic process theory and, in particular, Markov chains. The next chapter, “Relational proof systems for applied temporal logics” by E. Orlowska (pp. 249-277), provides an interpretation of temporal logics within a relational logic, the formalization of which is based on relational algebras. The final chapter, “An analysis of structure of time in the first order predicate calculus” by E. Hajnicz (pp. 279-322), analyzes various axiomatizations of time structures and their mutual translatability. In particular, both point and interval structures are characterized and compared within the framework of classical first-order predicate logic.

MSC:

03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
00B25 Proceedings of conferences of miscellaneous specific interest
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite