Abstract
Multi-valued systems are systems in which the atomic propositions and the transitions are not Boolean and can take values from some set. Latticed systems, in which the elements in the set are partially ordered, are useful in abstraction, query checking, and reasoning about multiple view-points. For example, abstraction involves systems in which an atomic proposition can take values from {true, unknown, false}, and these values can be partially ordered according to a “being more true” order (true ≥ unknown ≥ false) or according to a “being more informative” order (true ≥ unknown and false ≥ unknown). For Boolean temporal logics, researchers have developed a rich and beautiful theory that is based on viewing formulas as descriptors of languages of infinite words or trees. This includes a relation between temporal-logic formulas and automata on infinite objects, a theory of simulation relation between systems, a theory of two-player games, and a study of the relations among these notions. The theory is very useful in practice, and is the key to almost all algorithms and tools we see today in verification.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Lustig, Y. (2008). Multi-valued Logics, Automata, Simulations, and Games. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2008. Lecture Notes in Computer Science, vol 4905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78163-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-78163-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78162-2
Online ISBN: 978-3-540-78163-9
eBook Packages: Computer ScienceComputer Science (R0)