We consider the task of model building and model checking for temporal logic specifications over general linear flows of time. We present a new notation for giving a detailed description of the compositional construction of such a model and an efficient procedure for finding it from the temporal specification. We then also present an algorithm for checking whether a particular temporal formula holds in a general linear model. Applications include reasoning about distributed and concurrent systems, multi-agent systems, and understanding natural language. © 2013 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
French, T., McCabe-Dansted, J., & Reynolds, M. (2013). Indiscrete models: Model building and model checking over linear time. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7750 LNCS, pp. 50–68). Springer Verlag. https://doi.org/10.1007/978-3-642-36039-8_6
Mendeley helps you to discover research relevant for your work.