Skip to main content

Über dieses Buch

This volume contains the post-proceedings of the 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2012, held in Znojmo, Czech Republic, in October, 2012. The 13 thoroughly revised papers were carefully selected out of 31 submissions and are presented together with 6 invited papers. The topics covered by the papers include: computer-aided analysis and verification, applications of game theory in computer science, networks and security, modern trends of graph theory in computer science, electronic systems design and testing, and quantum information processing.



BDD-Based Software Model Checking with CPAchecker

In symbolic software model checking, most approaches use predicates as symbolic representation of the state space, and SMT solvers for computations on the state space; BDDs are sometimes used as auxiliary data structure. The representation of software state spaces by BDDs was not yet thoroughly investigated, although BDDs are successful in hardware verification. The reason for this is that BDDs do not efficiently support all operations that are needed in software verification. In this work, we evaluate the use of a pure BDD representation of integer variable values, and focus on a particular class of programs: event-conditionaction systems with limited operations. A symbolic representation using BDDs seems appropriate for this particular class of programs. We implement a program analysis based on BDDs and experimentally compare three symbolic techniques to verify reachability properties of ECA programs. The results show that BDDs are efficient, which yields the insight that BDDs could be used selectively for some variables (to be determined by a pre-analysis), even in general software model checking.
Dirk Beyer, Andreas Stahlbauer

Security for Cyber-Physical Systems

(Extended Abstract)
Cyber-physical systems are characterized by an IT infrastructure controlling effects in the physical world. Attacks are intentional actions trying to cause undesired effects in the physical world. We examine to which extent traditional IT security techniques can protect against attacks on cyber-physical systems and which additional measures could be deployed to strengthen their security. Properties relevant in this context are the veracity and plausibility of the data being processed.
Dieter Gollmann

Quantum Secret Sharing with Graph States

We study the graph-state-based quantum secret sharing protocols [24,17] which are not only very promising in terms of physical implementation, but also resource efficient since every player’s share is composed of a single qubit. The threshold of a graph-state-based protocol admits a lower bound: for any graph of order n, the threshold of the corresponding n-player protocol is at least 0.506n. Regarding the upper bound, lexicographic product of the C 5 graph (cycle of size 5) are known to provide n-player protocols which threshold is n − n 0.68. Using Paley graphs we improve this bound to n − n 0.71. Moreover, using probabilistic methods, we prove the existence of graphs which associated threshold is at most 0.811n.Albeit non-constructive, probabilistic methods permit to prove that a random graph G of order n has a threshold at most 0.811n with high probability. However, verifying that the threshold of a given graph is acually smaller than 0.811n is hard since we prove that the corresponding decision problem is NP-Complete.These results are mainly based on the graphical characterization of the graph-state-based secret sharing properties, in particular we point out strong connections with domination with parity constraints.
Sylvain Gravier, Jérôme Javelle, Mehdi Mhalla, Simon Perdrix

Testing Embedded Memories: A Survey

According to the International Technology Roadmap for Semiconductors, embedded memories will continue to dominate the increasing system on chips (SoCs) content in the future, approaching 90% in in some cases. Therefore, the memory yield and quality will have a dramatic impact on the overall SoC cost and outgoing product quality. Meeting a high memory yield and quality requires understanding memory designs, modeling their faulty behaviors in appropriate and accurate way, designing adequate tests and diagnosis strategies as well as efficient Design-for-Testability and Built-In-Self-Test (BIST) schemes. This paper presents the state of art in memory testing including fault modeling, test design and BIST. Further research challenges and opportunities are discussed in enabling testing (embedded) memories in the nano-era.
Said Hamdioui

Quicksort and Large Deviations

Quicksort may be the most familiar and important randomised algorithm studied in computer science. It is well known that the expected number of comparisons on any input of n distinct keys is Θ(n ln n), and the probability of a large deviation above the expected value is very small. This probability was well estimated some time ago, with an ad-hoc proof: we shall revisit this result in the light of further work on concentration.
Colin McDiarmid

Recent Results on Howard’s Algorithm

Howard’s algorithm is a fifty-year old generally applicable algorithm for sequential decision making in face of uncertainty. It is routinely used in practice in numerous application areas that are so important that they usually go by their acronyms, e.g., OR, AI, and CAV. While Howard’s algorithm is generally recognized as fast in practice, until recently, its worst case time complexity was poorly understood. However, a surge of results since 2009 has led us to a much more satisfactory understanding of the worst case time complexity of the algorithm in the various settings in which it applies. In this talk, we shall survey these recent results and the open problems that remains.
Peter Bro Miltersen

Advantage of Quantum Strategies in Random Symmetric XOR Games

Non-local games are known as a simple but useful model which is widely used for displaying nonlocal properties of quantum mechanics. In this paper we concentrate on a simple subset of non-local games: multiplayer XOR games with 1-bit inputs and 1-bit outputs which are symmetric w.r.t. permutations of players.
We look at random instances of non-local games from this class. We prove a tight bound for the expected performance on the classical strategies for a random non-local game and provide numerical evidence that quantum strategies achieve better results.
Andris Ambainis, Jānis Iraids, Dmitry Kravchenko, Madars Virza

Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed in the verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space. We document the efficiency of the algorithm by experiments comparing its performance with the state-of-the-art model checker UPPAAL.
Mathias Andersen, Heine Gatten Larsen, Jiří Srba, Mathias Grund Sørensen, Jakob Haahr Taankvist

Fast Algorithm for Rank-Width

Inspired by the heuristic algorithm for boolean-width by Telle et. al. [1], we develop a heuristic algorithm for rank-width. We compare results on graphs of practical relevance to the established bounds of boolean-width. While the width of most graphs is lower than the known values for tree-width, it turns out that the boolean-width heuristic is able to find decompositions of significantly lower width. In a second step we therefore present a further algorithm that can decide if for a graph G and a value k exists a rank-decomposition of width lower than k. This enables to show that boolean-width is in fact lower than or equal to rank-width on many of the investigated graphs.
Martin Beyß

Determinacy in Stochastic Games with Unbounded Payoff Functions

We consider infinite-state turn-based stochastic games of two players, □ and \(\Diamond\), who aim at maximizing and minimizing the expected total reward accumulated along a run, respectively. Since the total accumulated reward is unbounded, the determinacy of such games cannot be deduced directly from Martin’s determinacy result for Blackwell games. Nevertheless, we show that these games are determined both for unrestricted (i.e., history-dependent and randomized) strategies and deterministic strategies, and the equilibrium value is the same. Further, we show that these games are generally not determined for memoryless strategies. Then, we consider a subclass of \(\Diamond\) -finitely-branching games and show that they are determined for all of the considered strategy types, where the equilibrium value is always the same. We also examine the existence and type of (ε-)optimal strategies for both players.
Tomáš Brázdil, Antonín Kučera, Petr Novotný

Strategy Complexity of Finite-Horizon Markov Decision Processes and Simple Stochastic Games

Markov decision processes (MDPs) and simple stochastic games (SSGs) provide a rich mathematical framework to study many important problems related to probabilistic systems. MDPs and SSGs with finite-horizon objectives, where the goal is to maximize the probability to reach a target state in a given finite time, is a classical and well-studied problem. In this work we consider the strategy complexity of finite-horizon MDPs and SSGs. We show that for all ε > 0, the natural class of counter-based strategies require at most \(\log \log (\frac{1}{\epsilon}) + n+1\) memory states, and memory of size \(\Omega(\log \log (\frac{1}{\epsilon}) + n)\) is required, for ε-optimality, where n is the number of states of the MDP (resp. SSG). Thus our bounds are asymptotically optimal. We then study the periodic property of optimal strategies, and show a sub-exponential lower bound on the period for optimal strategies.
Krishnendu Chatterjee, Rasmus Ibsen-Jensen

Controllable-Choice Message Sequence Graphs

We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization.
Martin Chmelík, Vojtěch Řehák

A Better Way towards Key Establishment and Authentication in Wireless Sensor Networks

In this paper, we show that a previously published paper proposing both key establishment and node authentication protocols actually fails to provide the much needed security. In particular, we show a number of ways to compromise these protocols. To overcome flaws of these protocols, we propose novel protocols that remedy all the found security problems of the previous ones. Additionally, our proposals are by the state of the art computationally, energy and memory efficient.
Filip Jurnečka, Vashek Matyáš

Parameterized Algorithms for Stochastic Steiner Tree Problems

We consider the Steiner tree problem in graphs under uncertainty, the so-called two-stage stochastic Steiner tree problem (SSTP). The problem consists of two stages: In the first stage, we do not know which nodes need to be connected. Instead, we know costs at which we may buy edges, and a set of possible scenarios one of which will arise in the second stage. Each scenario consists of its own terminal set, a probability, and second-stage edge costs. We want to find a selection of first-stage edges and second-stage edges for each scenario that minimizes the expected costs and satisfies all connectivity requirements. We show that SSTP is in the class of fixed-parameter tractable problems (FPT), parameterized by the number of terminals. Additionally, we transfer our results to the directed and the prize-collecting variant of SSTP.
Denis Kurz, Petra Mutzel, Bernd Zey

Action Investment Energy Games

We introduce the formalism of action investment energy games where we study the trade-off between investments limited by given budgets and resource constrained (energy) behavior of the underlying system. More specifically, we consider energy games extended with costs of enabling actions and fixed budgets for each player. We ask the question whether for any Player 2 investment there exists a Player 1 investment such that Player 1 wins the resulting energy game. We study the action investment energy game for energy intervals with both upper and lower bounds, and with a lower bound only, and give a complexity results overview for the problem of deciding the winner in the game.
Kim G. Larsen, Simon Laursen, Jiří Srba

Ciphertext-Only Attack on Gentry-Halevi Implementation of Somewhat Homomorphic Scheme

In this paper we examine the first working implementation of a fully homomorphic scheme from C.Gentry and S.Halevi. We implemented the ciphertext-only attack from [2] using the NTL library and show that only dimensions up to 128 are feasible for common computational power. We propose also two improvements of this attack that enable us to use the fastest variant of LLL from NTL and compare the results.
Michal Mikuš, Marek Sýs

Grover’s Algorithm with Errors

Grover’s algorithm is a quantum search algorithm solving the unstructured search problem of size n in \(O(\sqrt{n})\) queries, while any classical algorithm needs O(n) queries [3].
However, if query has some small probability of failing (reporting that none of the elements are marked), then quantum speed-up disappears: no quantum algorithm can be faster than a classical exhaustive search by more than a constant factor [8].
We study the behaviour of Grover’s algorithm in the model there query may report some marked elements as unmarked (each marked element has its own error probability, independent of other marked elements).
We analyse the limiting behaviour of Grover’s algorithm for a large number of steps and prove the existence of limiting state ρ lim . Interestingly, the limiting state is independent of error probabilities of individual marked elements. If we measure ρ lim , the probability of getting one of the marked states i 1, …, i k is \(\frac{k}{k+1}\). We show that convergence time is O(n).
Andris Ambainis, Artūrs Bačkurs, Nikolajs Nahimovs, Alexander Rivosh

On WQO Property for Different Quasi Orderings of the Set of Permutations

The property of certain sets being well quasi ordered (WQO) has several useful applications in computer science – it can be used to prove the existence of efficient algorithms and also in certain cases to prove that a specific algorithm terminates.
One of such sets of interest is the set of permutations. The fact that the set of permutations is not WQO has been rediscovered several times and a number of different permutation antichains have been published. However these results apply to a specific ordering relation of permutations \(\preccurlyeq\), which is not the only ’natural’ option and an alternative ordering relation of permutations \(\trianglelefteq\) (more related to ’graph’ instead of ’sorting’ properties of permutations) is often of larger practical interest. It turns out that the known examples of antichains for the ordering \(\preccurlyeq\) can’t be used directly to establish that \(\trianglelefteq\) is not WQO.
In this paper we study this alternative ordering relation of permutations \(\trianglelefteq\) and give an example of an antichain with respect to this ordering, thus showing that \(\trianglelefteq\) is not WQO. In general antichains for \(\trianglelefteq\) cannot be directly constructed from antichains for \(\preccurlyeq\), however the opposite is the case – any antichain for \(\trianglelefteq\) allows to construct an antichain for \(\preccurlyeq\).
Sandra Ose, Juris Viksna

Towards User-Aware Multi-touch Interaction Layer for Group Collaborative Systems

State-of-the-art collaborative workspaces are represented either by large tabletops or wall-sized interactive displays. Extending bare multi-touch capability with metadata for association of touch events to individual users could significantly improve collaborative work of co-located group. In this paper, we present several techniques which enable development of such interactive environments. First, we describe an algorithm for scalable coupling of multiple touch sensors and a method allowing association of touch events with users. Further, we briefly discuss the Multi-Sensor (MUSE) framework which utilizes the two techniques and allows rapid development of touch-based user interface. Finally, we discuss the preliminary results of the prototype implementation.
Vít Rusňák, Lukáš Ručka, Petr Holub


Weitere Informationen

Premium Partner