×

zbMATH — the first resource for mathematics

Safety for branching time semantics. (English) Zbl 0769.68089
Automata, languages and programming, Proc. 18th Int. Colloq., Madrid/Spain 1991, Lect. Notes Comput. Sci. 510, 76-92 (1991).
Summary: [For the entire collection see Zbl 0753.00027.]
We study in a first part of this paper safety and liveness properties for any given program semantics. We give a topological definition of these properties using a safety preorder. Then, we consider the case of branching time semantics where a program is modeled by a set of infinite computation trees modulo bisimulation. We propose and study a safety preorder for this semantics based on simulation and dealing with silent actions. We focus on regular safety properties and characterize them by both tree-automata and formulas of a branching time logic. We show that verifying safety properties on trees reduces to simulation testing.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
03B70 Logic in computer science
PDF BibTeX XML Cite