Jiří Srba

TCS Journal 2018 Journal Article

Reachability problems: Special issue

• Kim G. Larsen
• Igor Potapov
• Jiří Srba

TCS Journal 2014 Journal Article

TCTL-preserving translations from timed-arc Petri nets to networks of timed automata

• Joakim Byg
• Morten Jacobsen
• Lasse Jacobsen
• Kenneth Yrke Jørgensen
• Mikael Harkjær Møller
• Jiří Srba

We present a framework for TCTL-preserving translations between time-dependent modeling formalisms. The framework guarantees that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioral equivalence between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischer's protocol, Lynch–Shavit protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability of the approach.

I&C Journal 2012 Journal Article

EXPTIME-completeness of thorough refinement on modal transition systems

• Nikola Beneš
• Jan Křetínský
• Kim G. Larsen
• Jiří Srba

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 and deterministic.

I&C Journal 2004 Journal Article

On the computational complexity of bisimulation, redux

• Faron Moller
• Scott Smolka
• Jiří Srba

Paris Kanellakis and the second author (Smolka) were among the first to investigate the computational complexity of bisimulation, and the first and third authors (Moller and Srba) have long-established track records in the field. Smolka and Moller have also written a brief survey about the computational complexity of bisimulation [ACM Comput. Surv. 27(2) (1995) 287]. The authors believe that the special issue of Information and Computation devoted to PCK50: Principles of Computing and Knowledge: Paris C. Kanellakis Memorial Workshop represents an ideal opportunity for an up-to-date look at the subject.