Dear Spiral User, we appreciate your patience during this upgrade which is to benefit our userbase, improve their experience in Spiral, introduce improvements, fixes and maintaining our versioning for future updates. Please note if you encounter any issues in Spiral, please raise a ticket to Research Applications team providing as much detail as possible in order to help us resolve your query. Again, we thank you for your patience and support during the upgrade. Kind Regards, Spiral Upgrade Team.
 
On model checking multiple hybrid views
File(s)
DTR04-6.pdf (277.3 KB)
Published version
Author(s)
Hussain, Altaf
Huth, Michael
Type
Report
Abstract
We study consistency, satis¯ability, and validity problems for
collectively model checking a set of views endowed with labelled transi-
tions, hybrid constraints on states, and atomic propositions. A PTIME
algorithm for deciding whether a set of views has a common re¯nement
(consistency) is given. We prove that deciding whether a common re¯ne-
ment satis¯es a formula of the hybrid mu-calculus (satis¯ability), and its
dual (validity), are EXPTIME-complete. We determine two generically
generated \summary" views that constitute informative and consistent
common re¯nements and abstractions of a set of views (respectively).
Date Issued
2004-01-01
Citation
Departmental Technical Report: 04/6, 2004, pp.1-15
URI
DOI
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
15
Journal / Book Title
Departmental Technical Report: 04/6
Copyright Statement
© 2004 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Copyright URL
Publication Status
Published
Article Number
04/6