Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userUndecidability of model-checking branching-time properties of stateless probabilistic pushdown process
336
0
0.0
(
0
)
Added by
Tianrong Lin
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Authors
Tianrong Lin
Ask ChatGPT about the research
No Arabic abstract
In this paper, we settle a problem in probabilistic verification of infinite--state process (specifically, {it probabilistic pushdown process}). We show that model checking {it stateless probabilistic pushdown process} (pBPA) against {it probabilistic computational tree logic} (PCTL) is undecidable.
rate research
Read More
In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.
This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal mu-calculus, three main problems: model-checking, logical reflection (aka global model-checking, that asks for a finite description of the set of elements for which a formula holds) and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems we provide an effective solution. This is obtained thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.
In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central importance. Traditionally, such requirements have been model-checked via a reduction to the unbounded case by unfolding the model according to the cost bound. This exacerbates the state space explosion problem and significantly increases runtime. In this paper, we present three new algorithms to model-check time- and cost-bounded properties for Markov decision processes and probabilistic timed automata that avoid unfolding. They are based on a modified value iteration process, on an enumeration of schedulers, and on state elimination techniques. We can now obtain results for any cost bound on a single state space no larger than for the corresponding unbounded or expected-value property. In particular, we can naturally compute the cumulative distribution function at no overhead. We evaluate the applicability and compare the performance of our new algorithms and their implementation on a number of case studies from the literature.
The paper describes an abstraction for protocols that are based on multiple rounds of Chaums Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.
194 -
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
