arXiv subjects

Harald Ruess

Publications and source records attributed to Harald Ruess.

25 records · Page 2Linked to original sources

arXiv2014

Certification for mu-calculus with winning strategies

We define memory-efficient certificates for $μ$-calculus model checking problems based on the well-known correspondence of the $μ$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of $μ$-calculus. We instrument the usual fixpoint iteration of $μ$-calculus model checking so that it produces evidence in the form of a winning strategy; these winning strategies can be computed in polynomial time in $|S|$ and in space $O(|S|^2 |ϕ|^2)$, where $|S|$ is the size of the state space and $|ϕ|$ the length of the formula $ϕ$\@. The main technical contribution here is the notion and algebra of partial winning strategies. On the technical level our work can be seen as a new, simpler, and immediate constructive proof of the correspondence between $μ$-calculus and parity games.

cs.LO↗

arXiv2013

Security policies for distributed systems

A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run in separation, and possible process communication on a technical platform is restricted to specified message paths of the system. Furthermore, we propose to further restrict the allowable information flow by adding filter functions for controlling which messages may be transmitted between processes, and we prove that locally checking filter functions is sufficient for ensuring global security policies. Altogether, global intransitive security policies are established by means of local verification conditions for the (trusted) processes of the distributed system. Moreover, security policies may be implemented securely on distributed integration platforms which ensure partitioning. We illustrate our results with a smart grid case study, where we use CTL model checking for discharging local verification conditions for each process under consideration.

cs.CR↗

arXiv2013

EFSMT: A Logical Framework for Cyber-Physical Systems

The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework and foundation for analyzing and synthesizing cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems in this paper include synthesis for robust control via BIBO stability, Lyapunov coefficient finding for nonlinear control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems. We are also proposing an algorithm for solving EFSMT problems based on the interplay between two SMT solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used techniques in modern SMT solvers, and generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic constraints.

cs.LO↗

arXiv2012

Distributed Priority Synthesis

Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables. We analyze the complexity of the problem, and propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into the VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics.

eess.SY↗

arXiv2012

Distributed Priority Synthesis and its Applications

Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables; this problem is NP-complete. We propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into our VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics.

cs.LO↗

arXiv2011

Algorithms for Synthesizing Priorities in Component-based Systems

We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis.

cs.LO↗

arXiv2010

A Game-theoretic Approach for Synthesizing Fault-Tolerant Embedded Systems

In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The result of the game is translated back to executable code concretizing fault-tolerant mechanisms using constraint solving. The overall approach is implemented to a prototype tool chain and is illustrated using examples.

cs.GT↗