2015 15th International Conference on Application of Concurrency to System Design (ACSD) (2015)
June 21, 2015 to June 26, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2015.18
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  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.
Lattices, Concrete, Reactive power, Model checking, Concurrent computing, System analysis and design, Encoding
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.