The Community for Technology Leaders
2015 15th International Conference on Application of Concurrency to System Design (ACSD) (2015)
Brussels, Belgium
June 21, 2015 to June 26, 2015
ISSN: 1550-4808
ISBN: 978-1-4673-7882-6
pp: 70-79
ABSTRACT
In model checking, abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on a multi-valued logic can distinguish between conclusive and inconclusive results, provides increased precision, and allows for encoding additional information into the model, which gives rise to new applications. To ensure a correct abstraction, one can use a mixed simulation [1] to relate a multi-valued model to its abstraction. In this paper we extend the notion of mixed simulation to include inconsistent values, thereby resolving an asymmetry in the definition and allowing for abstractions with increased precision when inconsistent values are available.
INDEX TERMS
Lattices, Concrete, Reactive power, Model checking, Concurrent computing, System analysis and design, Encoding
CITATION

S. Vijzelaar and W. Fokkink, "Multi-valued Abstraction Using Lattice Operations," 2015 15th International Conference on Application of Concurrency to System Design (ACSD), Brussels, Belgium, 2015, pp. 70-79.
doi:10.1109/ACSD.2015.18
95 ms
(Ver 3.3 (11022016))