This paper introduces temporal-logic queries for model understanding and model checking. A temporal-logic query is a temporal-logic formula in which a placeholder appears exactly once. Given a model, the semantics of a query is a proposition that can replace the placeholder to result in a formula that holds in the model and is as strong as possible. The author defines a class of CTL queries that can be evaluated in linear time, and show how they can be used to help the user understand the system behaviors and obtain more feedback in model checking.
CITATION STYLE
Chan, W. (2000). Temporal-logic queries. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1855, pp. 450–463). Springer Verlag. https://doi.org/10.1007/10722167_34
Mendeley helps you to discover research relevant for your work.