- e-mail:
- xbenes3(a)fi.muni.cz

by *
Peter Bezděk,
Nikola Beneš,
Vojtěch Havel,
Jiří Barnat,
Ivana Černá,
* A full version of the paper presented at conference ICTAC 2014. June 2014, 27 pages.

**FIMU-RS-2014-04.**
Available as *Postscript*,
**PDF**.

We introduce the *Clock-Aware Linear Temporal Logic* (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a~timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.

by *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at ICTAC 2012. June 2012, 25 pages.

**FIMU-RS-2012-02.**
Available as *Postscript*,
**PDF**.

We consider modal transition systems with infinite state space generated by finite sets of rules. In particular, we extend process rewrite systems to the modal setting and investigate decidability of the modal refinement relation between systems from various subclasses. Since already simulation is undecidable for most of the cases, we focus on the case where either the refined or the refining process is finite. Namely, we show decidability for pushdown automata extending the non-modal case and surprising undecidability for basic parallel processes. Further, we prove decidability when both systems are visibly pushdown automata. For the decidable cases, we also provide complexities. Finally, we discuss a notion of bisimulation over MTS.

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

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.

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

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

by *
Nikola Beneš,
Ivana Černá,
Jan Křetínský,
* November 2010, 44 pages.

**FIMU-RS-2010-12.**
Available as *Postscript*,
**PDF**.

Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we show that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we give a solution to the common implementation and specification problems lowering the complexity from EXPTIME to PTIME. Secondly, we identify a fundamental error made in previous attempts at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition.

by *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at MEMICS 2010. September 2010, 15 pages.

**FIMU-RS-2010-11.**
Available as *Postscript*,
**PDF**.

The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged.

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

Modal transition systems (MTS), a specification

by *
Nikola Beneš,
Luboš Brim,
Ivana Černá,
Jiří Sochor,
Pavlína Vařeková,
Barbora Zimmerová,
* July 2008, 21 pages.

**FIMU-RS-2008-07.**
Available as *Postscript*,
**PDF**.

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.