Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userComplexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
206
0
0.0
(
0
)
Added by
Naoki Kobayashi
Publication date
2011
fields
Informatics Engineering
and research's language is
English
Authors
Naoki Kobayashi
Ask ChatGPT about the research
No Arabic abstract
Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees generated by order-n recursion schemes is n-EXPTIME complete. We consider two subclasses of APT and investigate the complexity of the respective acceptance problems. The main results are that, for APT with a single priority, the problem is still n-EXPTIME complete; whereas, for APT with a disjunctive transition function, the problem is (n-1)-EXPTIME complete. This study was motivated by Kobayashis recent work showing that the resource usage verification of functional programs can be reduced to the model checking of recursion schemes. As an application, we show that the resource usage verification problem is (n-1)-EXPTIME complete.
rate research
Read More
188 -
Martin Lange (School of Electrical Engineering
, Computer Science
, n University of Kassel
2012
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 problem that 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.
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Ruttens behavioural differential equations.
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.
Higher-order recursion schemes are recursive equations defining new operations from given ones called terminals. Every such recursion scheme is proved to have a least interpreted semantics in every Scotts model of lambda-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite lambda-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in lambda-calculus by an endofunctor Hlambda and they explained simultaneous substitution of lambda-terms by proving that the presheaf of lambda-terms is an initial Hlambda-monoid. Here we work with the presheaf of rational infinite lambda-terms and prove that this is an initial iterative Hlambda-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.
A (fragment of a) process algebra satisfies unique parallel decomposition if the definable behaviours admit a unique decomposition into indecomposable parallel components. In this paper we prove that finite processes of the pi-calculus, i.e. processes that perform no infinite executions, satisfy this property modulo strong bisimilarity and weak bisimilarity. Our results are obtained by an application of a general technique for establishing unique parallel decomposition using decomposition orders.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
