eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
0
0
10.4230/OASIcs.MEMICS.2009
article
OASIcs, Volume 13, MEMICS'09, Complete Volume
Hlinený, Petr
Matyáš, Václav
Vojnar, Tomáš
OASIcs, Volume 13, MEMICS'09, Complete Volume
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/OASIcs.MEMICS.2009/OASIcs.MEMICS.2009.pdf
Mathematics of Computing, Physical Sciences and Engineering
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
i
vi
10.4230/DROPS.MEMICS.2009.2342
article
Preface -- Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)
Hlinený, Petr
Matyáš, Václav
Vojnar, Tomáš
The 2009 edition of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) is the fifth in a~row of three-day workshops organized in South Moravia by Faculty of Information Technology of Brno University of Technology and Faculty of Informatics of Masaryk University.
MEMICS'09 was held in Znojmo, Czech Republic, on November 13--15, 2009.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2342/DROPS.MEMICS.2009.2342.pdf
MEMICS 2009
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
1
9
10.4230/DROPS.MEMICS.2009.2355
article
A Privacy-Aware Protocol for Sociometric Questionnaires
Novotný, Marián
In the paper we design a protocol for sociometric questionnaires, which serves the privacy of responders. We propose a representation of a sociogram by a weighted digraph and interpret individual and collective phenomena of sociometry in terms of graph theory. We discuss security requirements for a privacy-aware protocol for sociometric questionnaires. In the scheme we use additively homomorphic public key cryptosystem, which allows single multiplication. We present the threshold version of the public key system and define individual phases of the scheme. The proposed protocol ensures desired security requirements and can compute sociometric indices without revealing private information about choices of responders.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2355/DROPS.MEMICS.2009.2355.pdf
Sociometry
sociogram
privacy
homomorphic encryption
security protocols
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
10
17
10.4230/DROPS.MEMICS.2009.2345
article
A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic
Larsen, Kim G.
Fahrenberg, Uli
Thrane, Claus
We extend the usual notion of Kripke Structures with a weighted transition relation, and generalize the usual Boolean satisfaction relation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax, and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2345/DROPS.MEMICS.2009.2345.pdf
Quantitative analysis
Kripke structures
characteristic formulae
bisimulation distance
weighted CTL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
18
26
10.4230/DROPS.MEMICS.2009.2349
article
Comparison of Algorithms for Checking Emptiness on Büchi Automata
Gaiser, Andreas
Schwoon, Stefan
We re-investigate the problem of LTL model-checking for finite-state systems. Typical solutions, like in Spin, work on the fly, reducing the problem to Büchi emptiness. This can be done in linear time, and a variety of algorithms with this property exist. Nonetheless, subtle design decisions can make a great difference to their actual performance in practice, especially when used on-the-fly. We compare a number of algorithms experimentally on a large benchmark suite, measure their actual run-time performance, and propose improvements. Compared with the algorithm implemented in Spin, our best algorithm is faster by about 33 % on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2349/DROPS.MEMICS.2009.2349.pdf
LTL Model checking
Depth first search
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
27
36
10.4230/DROPS.MEMICS.2009.2351
article
Derivation in Scattered Context Grammar via Lazy Function Evaluation
Jirák, Ota
Kolář, Dušan
This paper discusses scattered context grammars (SCG) and considers the application of scattered context grammar production rules. We use function that represents single derivation step over the given sentential form. Moreover, we define this function in such a way, so that it represents the delayed execution of scattered context grammar production rules using the same principles as a lazy evaluation in functional programming. Finally, we prove equivalence of the usual and the delayed execution of SCG production rules.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2351/DROPS.MEMICS.2009.2351.pdf
SCG
delayed execution
derivation
lazy evaluation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
37
44
10.4230/DROPS.MEMICS.2009.2353
article
Embedded Process Functional Language
Bĕhálek, Marek
Šaloun, Petr
Embedded systems represent an important area of computer engineering. Demands on embedded applications are increasing. To address these issues, different agile methodologies are used in traditional desktop applications today. These agile methodologies often try to eliminate development risks in early design phases. Possible solution is to create a working model or a prototype of critical system parts. Then we can use this prototype in negotiation with customer and also to prove technological aspects of our solution. From this perspective functional languages are very attractive. They have excellent abstraction mechanism and they can be used as a tool producing a kind of executable design. In this paper we present our work on a domain specific functional language targeted to embedded systems Embedded process functional language. Created language works on a high level of abstraction and it uses other technologies (even other functional languages) created for embedded systems development on lower levels. It can be used like a modeling or a prototyping language in early development phases.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2353/DROPS.MEMICS.2009.2353.pdf
Embedded systems
model
high abstraction level
functional programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
45
52
10.4230/DROPS.MEMICS.2009.2343
article
Exact Quantum Query Algorithm for Error Detection Code Verification
Vasilieva, Alina
Quantum algorithms can be analyzed in a query model to compute Boolean functions.
Function input is provided in a black box, and the aim is to compute the function value using as few queries to the black box as possible.
A repetition code is an error detection scheme that repeats each bit of the original message r times.
After a message with redundant bits is transmitted via a communication channel, it must be verified.
If the received message consists of r-size blocks of equal bits, the conclusion is that there were no errors.
The verification procedure can be interpreted as an application of a query algorithm, where input is a message to be checked.
Classically, for N-bit message, values of all N variables must be queried. We demonstrate an exact quantum algorithm that uses only N/2 queries.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2343/DROPS.MEMICS.2009.2343.pdf
Quantum computing
quantum query algorithms
algorithm complexity
Boolean functions
algorithm design
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
53
61
10.4230/DROPS.MEMICS.2009.2348
article
Faster Algorithm for Mean-Payoff Games
Chaloupka, Jakub
Brim, Luboš
We study some existing techniques for solving mean-payoff games (MPGs),
improve them, and design a randomized algorithm for solving MPGs with
currently the best expected complexity.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2348/DROPS.MEMICS.2009.2348.pdf
Mean-payoff games
randomized algorithms
computational complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
62
69
10.4230/DROPS.MEMICS.2009.2347
article
One size does not fit all - how to approach intrusion detection in wireless sensor networks
Stetsko, Andriy
Matyáš, Václav
A wireless sensor network (WSN) is a highly distributed network of resource constrained and wireless devices called sensor nodes. In the work we consider intrusion detection systems as they are proper mechanisms to defend internal attacks on WSNs. A wide diversity of WSN applications on one side and limited resources on other side implies that "one-fit-all" intrusion detection system is not optimal. We present a conceptual proposal for a suite of tools that enable an automatic design of intrusion detection system that will be (near) optimal for a given network topology, capabilities of sensor nodes and anticipated attacks.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2347/DROPS.MEMICS.2009.2347.pdf
Intrusion detection
wireless sensor networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
70
79
10.4230/DROPS.MEMICS.2009.2356
article
Rewriting Systems over Nested Data Words
Bouajjani, Ahmed
Drăgoi, Cezara
Jurski, Yan
Sighireanu, Mihaela
We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be
effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2356/DROPS.MEMICS.2009.2356.pdf
Nested data words
rewriting systems
program verification
dynamic and parametrized systems
invariance checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
80
87
10.4230/DROPS.MEMICS.2009.2354
article
Space Effective Model Checking for Component-Interaction Automata
Beneš, Nikola
Křivánek, Milan
Štefaňák, Filip
The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic. As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample set partial order reduction method within the component-interaction automata verification framework. Due to the state and action-based nature of both the modelling and specification formalisms, the implementation differs from traditional state-based approaches. After describing the implementation, we present some of the results obtained by employing the enhanced verification framework on a case study.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2354/DROPS.MEMICS.2009.2354.pdf
Model checking
component-based systems
partial order reduction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
88
95
10.4230/DROPS.MEMICS.2009.2350
article
The Parameterized Complexity of Oriented Colouring
Ganian, Robert
The oriented colouring problem is intuitive and related to
undirected colouring, yet remains NP-hard even on digraph classes
with bounded traditional directed width measures.
Recently we have also proved that it remains NP-hard
in otherwise severely restricted digraph classes.
However, unlike most other problems on directed graphs, the oriented colouring
problem is not directly transferable to undirected graphs.
In the article we look at the parameterized complexity of computing the oriented colouring
of digraphs with bounded undirected width parameters, whereas the parameters
``forget'' about the orientations of arcs and treat them as edges.
Specifically, we provide new complexity results for computing oriented colouring
on digraphs of bounded undirected rank-width and a new algorithm for this problem
on digraphs of bounded undirected tree-width.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2350/DROPS.MEMICS.2009.2350.pdf
Oriented colouring
tree-width
rank-width
parameterized algorithms
graphs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
96
105
10.4230/DROPS.MEMICS.2009.2352
article
Towards Comparing the Robustness of Synchronous and Asynchronous Circuits by Fault Injection
Jeitler, Marcus
Lechner, Jakob
As transient error rates are growing due to smaller feature sizes,
designing reliable synchronous circuits becomes increasingly
challenging. Asynchronous logic design constitutes a promising
alternative with respect to robustness and stability. In particular,
delay-insensitive asynchronous circuits provide interesting properties,
like an inherent resilience to delay-faults.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2352/DROPS.MEMICS.2009.2352.pdf
Four State Logic
Asynchronous Design
Fault Injection
Fault Tolerance
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
106
113
10.4230/DROPS.MEMICS.2009.2346
article
Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants
Jacobsen, Lasse
Jacobsen, Morten
Møller, Mikael H.
Timed-Arc Petri Nets (TAPN) is a well studied extension of the classical Petri net model where tokens are decorated with real numbers that represent their age. Unlike reachability, which is known to be undecidable for TAPN, boundedness and coverability remain decidable. The model is supported by a recent tool called TAPAAL which, among others, further extends TAPN with invariants on places in order to model urgency. The decidability of boundedness and coverability for this extended model has not yet been considered. We present a reduction from two-counter Minsky machines to TAPN with invariants to show that both the boundedness and coverability problems are undecidable.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2346/DROPS.MEMICS.2009.2346.pdf
Timed-Arc Petri Nets
Undecidability
Coverability
Boundedness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2009-12-15
13
114
121
10.4230/DROPS.MEMICS.2009.2344
article
Weighted Dynamic Pushdown Networks
Wenner, Alexander
We develop a generic framework for the analysis of programs with recursive procedures and dynamic process creation. To this end we combine the approach of weighted pushdown systems (WPDS) with the model of dynamic pushdown networks (DPN). Weighted dynamic pushdown networks (WDPN) describe processes running in parallel. Each process may perform pushdown actions and spawn new processes. Transitions are labelled by weights to carry additional information. We derive a method to determine meet-over-all-paths values for the paths from a starting configuration to a regular set of configurations of a WDPN.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol013-memics2009/DROPS.MEMICS.2009.2344/DROPS.MEMICS.2009.2344.pdf
Program analysis
recursive procedures
dynamic process creation
dataflow analysis