A list with abstracts sorted by year - 2010
Disjunctive Modal Transition Systems and Generalized LTL Model Checking
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
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.
Computing Strongly Connected Components in Parallel on CUDA (full version)
The problem of decomposition of a directed graph into its strongly connected
A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking
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
One of the toughest problems to solve when
Security of Biometric Authentication Systems -- Extended Version
This technical report outlines our views of actual security
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.
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
Stochastic Real-Time Games with Qualitative Timed Automata Objectives
We consider two-player stochastic games over real-time probabilistic
Neighbor-Based Intrusion Detection for Wireless Sensor Networks
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
We design a novel algorithm for solving Mean-Payoff Games
Reachability Games on Extended Vector Addition Systems with States
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
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
Please install a newer browser for this site to function properly.