A List by Author: Vojtěch Řehák
- e-mail:
- rehak(a)fi.muni.cz
- home page:
- https://www.fi.muni.cz/~xrehak/
Verification of Open Interactive Markov Chains
by
Tomáš Brázdil,
Holger Hermanns,
Jan Krčál,
Jan Křetínský,
Vojtěch Řehák,
A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.
FIMU-RS-2012-04.
Available as Postscript,
PDF.
Abstract:
Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive
bounds on reachability probabilities that are assured to hold in any composition context.
Stochastic Real-Time Games with Qualitative Timed Automata Objectives
by
Tomáš Brázdil,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
Vojtěch Řehák,
A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.
FIMU-RS-2010-05.
Available as Postscript,
PDF.
Abstract:
We consider two-player stochastic games over real-time probabilistic
processes where the winning objective is specified by a timed
automaton. The goal of player I is to play in such a way that the
play (a timed word) is accepted by the timed automaton with probability
one. Player II aims at the opposite. We prove that whenever
player I has a winning strategy, then she also has a strategy that
can be specified by a timed automaton. The strategy automaton reads the
history of a play, and the decisions taken by the strategy depend only on
the region of the resulting configuration. We also give an
exponential-time algorithm which computes a winning timed automaton
strategy if it exists.
Decidable Race Condition for HMSC
by
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
December 2009, 30 pages.
FIMU-RS-2009-10.
Available as Postscript,
PDF.
Abstract:
Races in Message Sequence Charts may lead to a bad interpretation of
described behaviours, and are often considered as a design error. While
there is a quadratic-time algorithm detecting races in Basic Message
Sequence Charts (BMSCs), the problem is undecidable for High-level
Message Sequence Charts (HMSCs). To improve this negative situation for
HMSCs, we introduce two new notions: a new concept of race called
trace-race and an extension of the HMSC formalism with open coregions,
i.e. coregions that can extend over more than one BMSC. We present three
arguments showing benefits of our notions over the standard notions of
race and HMSC. First, every trace-race-free HMSC is also race-free.
Second, every race-free HMSC can be equivalently expressed as a
trace-race-free HMSC with open coregions. Last, the trace-race detection
problem for HMSC with open coregions is decidable and PSPACE-complete
(the problem is in P if the number of processes and gates is fixed).
Formalisms and Tools for Design and Specification of Network Protocols
by
Jindřich Babica,
Vojtěch Řehák,
Petr Slovák,
Pavel Troubil,
Martin Zavadil,
May 2007, 33 pages.
FIMU-RS-2007-02.
Available as Postscript,
PDF.
Abstract:
Message Sequence Charts (MSC) are a useful formalism for formalization of
network protocols early in their design phase. In this paper, we introduce
the basics of MSC language and describe some of the possibilities for
automatic location of "problematic" parts in the design. Focus is then given
to different modifications of MSC design (FIFO behavior, bounded channels,
etc. ) as well as formal checking of more complex design properties (MSC
membership, realizability). Next, an introduction of Specification and
Description Language (SDL) is presented. Possibilities of automatic
synthesis of system design in MSC to an SDL model and it`s correctness
verification are mentioned.
On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems
by
Laura Bozzelli,
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
A full version of the paper presented at FSTTCS 2006. November 2006, 27 pages.
FIMU-RS-2006-05.
Available as Postscript,
PDF.
Abstract:
We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities strict eventually and strict always. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.
Refining the Undecidability Border of Weak Bisimilarity
by
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
A full version of the paper presented at INFINITY 2005. August 2005, 20 pages.
FIMU-RS-2005-06.
Available as Postscript,
PDF.
Abstract:
Weak bisimilarity is one of the most studied behavioural equivalences. This
equivalence is undecidable for pushdown processes (PDA),
process algebras (PA), and multiset automata (MSA, also known
as parallel pushdown processes, PPDA). Its decidability is an open
question for basic process algebras (BPA) and basic parallel
processes (BPP). We move the undecidability border towards these classes
by showing that the equivalence remains undecidable for weakly extended
versions of BPA and BPP. Further, we show the results hold for even more
restricted classes of normed BPA with finite constraint system and normed
BPP with finite constraint system.
Process Rewrite Systems with Weak Finite-State Unit
by
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
This is a full version of the paper presented at INFINITY`03. September 2003, 23 pages.
FIMU-RS-2003-05.
Available as Postscript,
PDF.
Abstract:
Various classes of infinite-state processes are often specified by rewrite
systems. We extend Mayr`s Process Rewrite Systems (PRS) by finite-state unit
whose transition function satisfies some restrictions inspired by weak
finite automata. We classify these models by their expressiveness and show
how the hierarchy of new classes (w.r.t. bisimilarity) is related to both
PRS hierarchy of Mayr and two other hierarchies of PRS extensions introduced
in [JKM02, Str02].