Technical Reports

A list with abstracts sorted by year - 2010

Disjunctive Modal Transition Systems and Generalized LTL Model Checking

by Nikola Bene¹, Ivana Èerná, Jan Køetínský, November 2010, 44 pages.

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

Abstract:

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.

Process Algebra for Modal Transition Systemses

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.

Abstract:

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. Therefore, we introduce transition systems with obligations as a general model encompassing all the aforementioned models, and equip it with a process algebra description. Using these instruments, we then compare the previously studied subclasses and characterize their relationships.

Computing Strongly Connected Components in Parallel on CUDA (full version)

by Jiøí Barnat, Petr Bauch, Lubo¹ Brim, Milan Èe¹ka, July 2010, 24 pages.

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

Abstract:

The problem of decomposition of a directed graph into its strongly connected components is a fundamental graph problem inherently present in many scientific and commercial applications. In this paper we show how existing parallel algorithms can be reformulated in order to be accelerated by NVIDIA CUDA technology. In particular, we design a new CUDA-aware procedure for pivot selection and we redesign the parallel algorithms in order to allow for CUDA accelerated computation. We also experimentally demonstrate that with a single GTX 280 GPU card we can easily outperform optimal serial CPU implementation, which is particularly interesting result as unlike the serial CPU case, the asymptotic complexity of the parallel algorithms is not optimal.

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.

Access Rights in Enterprise Full-text Search

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.

Abstract:

One of the toughest problems to solve when deploying an enterprise-wide full-text search system is to handle the access rights of the documents and intranet web pages correctly and effectively. Post-processing the results of general-purpose full-text search engine (filtering out the documents inaccessible to the user who sent the query) can be an expensive operation, especially in large collections of documents. We discuss various approaches to this problem and propose a novel method which employs virtual tokens for encoding the access rights directly into the search index. We then evaluate this approach in an intranet system with several millions of documents and a complex set of access rights and access rules.

Security of Biometric Authentication Systems -- Extended Version

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.

Abstract:

This technical report outlines our views of actual security of biometric authentication and encryption systems. The attractiveness of some novel approaches like cryptographic key generation from biometric data is in some respect understandable, yet so far has lead to various shortcuts and compromises on security. The report starts with an introductory section that is followed by a section about variability of biometric characteristics, with a particular attention paid to biometrics used in large systems. The following sections then discuss the potential for biometric authentication systems, and for the use of biometrics in support of cryptographic applications as they are typically used in computer systems.

Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P

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.

Abstract:

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 (k-1)-EXPTIME. In this paper, we show that, for k = 2, the problem is in P, and thus improve the EXPTIME upper bound.

Stochastic Real-Time Games with Qualitative Timed Automata Objectives

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.

Abstract:

We consider two-player stochastic games over real-time probabilistic processes where the winning objective is specified by a timed automaton. The goal of player I is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player II aims at the opposite. We prove that whenever player I has a winning strategy, then she also has a strategy that can be specified by a timed automaton. The strategy automaton reads the history of a play, and the decisions taken by the strategy depend only on the region of the resulting configuration. We also give an exponential-time algorithm which computes a winning timed automaton strategy if it exists.

Neighbor-Based Intrusion Detection for Wireless Sensor Networks

by Andriy Stetsko, Luká¹ Folkman, Václav Matyá¹, May 2010, 33 pages.

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

Abstract:

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.

Using Strategy Improvement to Stay Alive

by Lubo¹ Brim, Jakub Chaloupka, March 2010, 48 pages.

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

Abstract:

We design a novel algorithm for solving Mean-Payoff Games (MPGs). Besides solving an MPG in the usual sense, our algorithm computes more information about the game, information that is important with respect to applications. The weights of the edges of an MPG can be thought of as a gained/consumed energy -- depending on the sign. For each vertex, our algorithm computes the minimum amount of initial energy that is sufficient for player Max to ensure that in a play starting from the vertex, the energy level never goes below zero. Our algorithm is not the first algorithm that computes the minimum sufficient initial energies, but according to our experimental study it is the fastest algorithm that computes them. The reason is that it utilizes the strategy improvement technique which is very efficient in practice.

Reachability Games on Extended Vector Addition Systems with States

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.

Abstract:

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.

Human Problem Solving: Sokoban Case Study

by Petr Jaru¹ek, Radek Pelánek, April 2010, 25 pages.

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

Abstract:

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 differences in problem difficulty.