Technical Reports

A List by Author: Jiøí Srba

e-mail:

srba(a)fi.muni.cz

home page:

https://www.fi.muni.cz/~srba/

Dual-Priced Modal Transition Systems with Time Durations

by Nikola Bene¹, Jan Køetínský, Kim Guldstrand Larsen, Mikael Moeller, Jiøí Srba, A full version of the paper presented at conference LPAR 2012. January 2012, 23 pages.

FIMU-RS-2012-01. Available as Postscript, PDF.

Abstract:

Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.

Parametric Modal Transition Systems

by Nikola Bene¹, Jan Køetínský, Kim Guldstrand Larsen, Mikael Moller, Jiøí Srba, A full version of the paper presented at ATVA 2011 July 2011, 24 pages.

FIMU-RS-2011-03. Available as Postscript, PDF.

Abstract:

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcome many of the limitations and we investigate the computational complexity of modal refinement checking.

A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

by Lasse Jacobsen, Morten Jacobsen, Mikael Moeller, Jiøí Srba, A full version of the paper presented at EPEW`10. August 2010, 34 pages.

FIMU-RS-2010-09. Available as Postscript, PDF.

Abstract:

Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.

An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata

by Joakim Byg, Kenneth Yrke Joergensen, Jiøí Srba, A full version of the paper presented at ICFEM`09. October 2009, 29 pages.

FIMU-RS-2009-06. Available as Postscript, PDF.

Abstract:

Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to net- works of timed automata, though the Petri net model cannot express urgent be- haviour and the described mutual translations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The trans- lation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.

Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

by Nikola Bene¹, Jan Køetínský, Kim Guldstrand Larsen, Jiøí Srba, A full version of the paper presented at conference ICTAC 2009. July 2009, 28 pages.

FIMU-RS-2009-03. Available as Postscript, PDF.

Abstract:

Modal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.

We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed.

Complexity Issues of the Pattern Equations in Idempotent Semigroups

by Ondøej Klíma, Jiøí Srba, August 1999, 14 pages.

FIMU-RS-99-02. Available as Postscript, PDF.

Abstract:

A pattern equation is a word equation of the form X=A where X is a sequence of variables and A is a sequence of constants. The problem whether X=A has a solution in a free idempotent semigroup (free band) is shown to be NP--complete.

On the Pattern Equations

by Ivana Èerná, Ondøej Klíma, Jiøí Srba, This is a full version of the paper accepted to SOFSEM`99. July 1999, 11 pages.

FIMU-RS-99-01. Available as Postscript, PDF.

Abstract:

Word equation in a special form X=A, where X is a sequence of variables and A is a sequence of constants, is considered. The problem whether X=A has a solution over a free monoid (PATTERN EQUATION problem) is shown to be NP--complete. It is also shown that disjunction of a special type equation systems and conjunction of the general ones can be eliminated. Finally, the case of stuttering equations where the word identity is read modulo xx=x is mentioned.

Comparing the Classes BPA and BPA with Deadlocks

by Jiøí Srba, This is a full version of the paper accepted to MFCS`98. June 1998, 36 pages.

FIMU-RS-98-05. Available as Postscript, PDF.

Abstract:

The class of BPA (or context-free) processes has been intensively studied and bisimilarity and regularity appeared to be decidable. We extend these processes with a deadlocking state into BPA_delta systems. We show that the BPA_delta class is more expressive w.r.t. bisimulation equivalence but it remains language equivalent to BPA. We prove that bisimilarity and regularity remain decidable in the BPA_delta class. Finally we give a characterisation of those BPA_delta processes which can be equivalently (up to bisimilarity) described within the "pure" BPA syntax.