A List by Author: Jan Strejček
- e-mail:
- xstrejc(a)fi.muni.cz
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).
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.
Characteristic Patterns for LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.
FIMU-RS-2004-10.
Available as Postscript,
PDF.
Abstract:
We give a new characterization of those languages that are definable
in fragments of LTL where the nesting depths of X and
U modalities are bounded by given constants. This brings further results
about various LTL fragments. We also propose a generic method for
decomposing LTL formulae into an equivalent disjunction of ``semantically
refined" LTL formulae, and indicate how this result can be used to
improve the functionality of existing LTL model-checkers.
Deeper Connections between LTL and Alternating Automata
by
Radek Pelánek,
Jan Strejček,
September 2004, 26 pages.
FIMU-RS-2004-08.
Available as Postscript,
PDF.
Abstract:
It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae
into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. We improve the latter translation and present deeper connections between LTL and A1W automata. Using these translations we identify the classes of A1W automata equivalent to LTL fragments given by
bounds on nesting depths of temporal operators (see,
e.g., [Wil99,KS02]) and the fragments of Until-Release
hierarchy [CP03].
An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator
by
Antonín Kučera,
Jan Strejček,
May 2004, 11 pages.
FIMU-RS-2004-04.
Available as Postscript,
PDF.
Abstract:
It is known that an LTL property is expressible by an LTL formula
without any next-time operator if and only if the property is
stutter invariant. It is also known that the problem whether a
given LTL property is stutter invariant is PSPACE-complete. We
extend these results to fragments of LTL obtained by restricting the
nesting depth of the next-time operator to a given n.
Some interesting facts about the logic LTL follow as simple
corollaries.
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].
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at CSL`02. July 2002, 24 pages.
FIMU-RS-2002-03.
Available as Postscript,
PDF.
Abstract:
It is known that LTL formulae without the `next` operator
are invariant under the so-called
stutter-equivalence of
words. In this paper we extend this principle to general
LTL formulae with given nesting depths of the `next` and `until` operators. This allows us to prove the semantical strictness of three
natural hierarchies of LTL formulae, which are
parametrized either
by the nesting depth of just one of the two operators,
or by both of them. As another interesting corollary
we obtain an alternative
characterization of LTL languages, which are exactly the
regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.
Constrained Rewrite Transition Systems
by
Jan Strejček,
December 2000, 30 pages.
FIMU-RS-2000-12.
Available as Postscript,
PDF.
Abstract:
We extend broadly studied rewrite transition systems with a mechanism for computing with partial information in the form similar to that one used in Concurrent Constraint Programming (CCP). Two new classes of transition systems (fcBPA and fcBPP) are introduced as this extension changes expressibility power of rewrite transition systems corresponding to BPA and BPP. The power of rewrite systems corresponding to other classes (FSA, PDA, PPDA, and PN) remains unchanged. The new classes are inserted to the hierarchy of standard process classes presented by Moller [Mol96].