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 Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka, July 2010, 24 pages.
FIMU-RS-2010-10. Available as Postscript, PDF.
The problem of decomposition of a directed graph into its strongly connected
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.
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.
by Jan Kasprzak, Michal Brandejs, Matěj Čuhel, Tomáš Obšívač, A full version of the paper presented at ICEIS 2010 conference. July 2010, 19 pages.
FIMU-RS-2010-08. Available as Postscript, PDF.
One of the toughest problems to solve when
by Václav Matyáš, Zdeněk Říha, A full version of the paper presented at conference Computer Information Systems and Industrial Management Applications 2010 June 2010, 27 pages.
FIMU-RS-2010-07. Available as Postscript, PDF.
This technical report outlines our views of actual security
by Jakub Chaloupka, A full version of the paper presented at Workshop on Reachability Problems 2010 August 2010, 36 pages.
FIMU-RS-2010-06. Available as Postscript, PDF.
We consider a two-player infinite game with zero-reachability objectives played on a 2-dimensional vector addition system with states (VASS), the states of which are divided between the two players. Brázdil, Jančar, and Kučera (2010) have shown that for k > 0, deciding the winner in a game on k-dimensional VASS is in
by Tomáš Brázdil, Jan Krčál, Jan Křetínský, Antonín Kučera, Vojtěch Řehák, A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.
FIMU-RS-2010-05. Available as Postscript, PDF.
We consider two-player stochastic games over real-time probabilistic
by Andriy Stetsko, Lukáš Folkman, Václav Matyáš, May 2010, 33 pages.
FIMU-RS-2010-04. Available as Postscript, PDF.
The neighbor-based detection technique explores the principle that sensor nodes situated spatially close to each other tend to have similar behavior. A node is considered malicious if its behavior significantly differs from its neighbors. The detection technique is localized, unsupervised and adapts to changing network dynamics. Although the technique is promising, it has not been deeply researched in the context of wireless sensor networks yet. In this technical report we analyze symptoms of different attacks for the applicability of the neighbor-based technique. The analysis shows that the technique can be used for detection of selective forwarding, jamming and hello flood attacks. We implemented an intrusion detection system which employs the neighbor-based detection technique. The system was designed for and works on the TinyOS operating system running the Collection tree protocol. We evaluated accuracy of the technique in detection of selective forwarding, jamming and hello flood attacks. The results show that the neighbor-based detection technique is highly accurate, especially in the case when collaboration among neighboring nodes is used.
by Luboš Brim, Jakub Chaloupka, March 2010, 48 pages.
FIMU-RS-2010-03. Available as Postscript, PDF.
We design a novel algorithm for solving Mean-Payoff Games
by Tomáš Brázdil, Petr Jančar, Antonín Kučera, A full version of the paper presented at ICALP 2010. February 2010, 38 pages.
FIMU-RS-2010-02. Available as Postscript, PDF.
We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.
by Petr Jarušek, Radek Pelánek, April 2010, 25 pages.
FIMU-RS-2010-01. Available as Postscript, PDF.
We describe a case study in human problem solving for a particular problem - a Sokoban puzzle. For the study we collected data using the Internet. In this way we were able to collect significantly larger data (2000 problems solved, 780 hours of problem solving activity) than in typical studies of human problem solving. Our analysis of collected data focuses on the issue of problem difficulty. We show that there are very large differences in difficulty of individual Sokoban problems and that these differences are not explained by previous research. To address this gap in understanding we describe an abstract computational model of human problem solving, a metric of a problem decomposition, and formalization of a state space bottleneck. We discuss how these concepts help us understand human problem solving activity and