by Tomáš Brázdil, Holger Hermanns, Jan Krčál, Jan Křetínský, Vojtěch Řehák, A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.
FIMU-RS-2012-04. Available as Postscript, PDF.
Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive
by Hannes Klarner, Adam Streck, David Šafránek, Juraj Kolcak, Heike Siebert, A full version of the paper presented at conference CMSB 2012. November 2012, 39 pages.
FIMU-RS-2012-03. Available as Postscript, PDF.
We propose a new methodology for identification and analysis of discrete gene networks as defined by Rene Thomas, supported by a tool chain: (i) given a Thomas network with partially known kinetic parameters, we reduce the number of acceptable parametrizations to those that fit time-series measurements and reflect other known constraints by an improved technique of coloured LTL model checking performing efficiently on Thomas networks in distributed environment; $(ii)$ we introduce classification of acceptable parametrizations to identify the most optimal ones; (iii) we propose a way of visualising parametrizations dynamics wrt time-series data. The methodology is validated on a rat neural development case study; (iv) finally we provide description of developed algorithms and evaluation of their performance.
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.