Deterministic CTL query solving

摘要

Temporal logic queries provide a natural framework to extend the realm of model checking from mere verification of engineers' specifications to computing previously unknown temporal properties of a system. Formally, temporal logic queries are patterns of temporal logic specifications which contain placeholders for subformulas; a solution to a temporal logic query is an instantiation which renders the specification true. In this paper, we investigate temporal logic queries that can be solved deterministically, i.e., solving such queries can be reduced in a deterministic manner to solving their subqueries at appropriate system states. We show that this kind of determinism is intimately related to the notion of intermediate collecting queries studied by the authors in previous work. We describe a large class of deterministically solvable CTL queries and devise a BDD-based symbolic algorithm for this class.