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.


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


Zbl 0753.00027