Paper Info
Title
Model-Checking The Higher-Dimensionalmodal Mu-Calculus
Abstract
The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in polynomial time, and conversely every polynomial-time decidable problemthat has a bisimulation-invariant encoding into labeled transition systems can also be defined in the higher-dimensional modal mu-calculus. We exemplify the latter connection by giving several examples of decision problems which reduce to model checking of the higher-dimensional modal mu-calculus for some fixed formulas. This way generic model checking algorithms for the logic can then be used via partial evaluation in order to obtain algorithms for theses problems which may benefit from improvements that are well-established in the field of program verification, namely on-the-fly and symbolic techniques. The aim of this work is to extend such techniques to other fields as well, here exemplarily done for process equivalences, automata theory, parsing, string problems, and games.
Year
DOI
Venue
2012
10.4204/EPTCS.77.6
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Combinatorics,Automata theory,Model checking,Algebra,Computer science,Finite element method,Invariant (mathematics),Bisimulation,Parsing,Modal,Calculus
Journal
77
Issue
ISSN
Citations 
77
2075-2180
3
PageRank 
References 
Authors
0.42
15
2
Name
Order
Citations
PageRank
Martin Lange144722.83
Étienne Lozes212114.32