Technical Reports

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].