56
IRUS TotalDownloads
Altmetric
Automata games for multiple-model checking
File | Description | Size | Format | |
---|---|---|---|---|
automata-games-multiple-views.pdf | 221.44 kB | Adobe PDF | View/Open |
Title: | Automata games for multiple-model checking |
Authors: | Hussain A Huth M |
Item Type: | Journal Article |
Abstract: | 3-valued models have been advocated as a means of system abstraction such that verifications and refutations of temporal-logic properties transfer from abstract models to the systems they represent. Some application domains, however, require multiple models of a concrete or virtual system. We build the mathematical foundations for 3-valued property verification and refutation applied to sets of common concretizations of finitely many models. We show that validity checking for the modal mu-calculus has the same cost (EXPTIME-complete) on such sets as on all 2-valued models, provide an efficient algorithm for checking whether common concretizations exist for a fixed number of models, and propose using parity games on variants of tree automata to efficiently approximate validity checks of multiple models. We prove that the universal topological model in [M. Huth, R. Jagadeesan, and D. A. Schmidt. A domain equation for refinement of partial systems. Mathematical Structures in Computer Science, 14(4):469-505, 5 August 2004] is not bounded complete. This confirms that the approximations aforementioned are reasonably precise only for tree-automata-like models, unless all models are assumed to be deterministic. © 2006 Elsevier B.V. All rights reserved. |
Issue Date: | 12-May-2006 |
Citation: | Electronic Notes in Theoretical Computer Science Vol.( 155 ) No.( ) pp 401 - 421 |
URI: | http://hdl.handle.net/10044/1/805 |
Publisher Link: | http://dx.doi.org/10.1016/j.entcs.2005.11.067 |
Start Page: | 401 |
End Page: | 421 |
Copyright Statement: | © 2006 Elsevier B.V. This is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, volume 155 (May 2006). doi:10.1016/j.entcs.2005.11.067 |
Volume: | 155 |
Appears in Collections: | Quantitative Analysis and Decision Science |