Search

Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. Our logic supports quantification over paths in a system - as is possible in hyperlogics such as HyperCTL* - but resolves the paths based on the strategic choices of a coalition of agents. This allows us to capture many previously studied (strategic) security notions in a unifying hyperlogic. Moreover, we show that HyperATL* is particularly useful for specifying asynchronous hyperproperties, i.e., hyperproperties where the execution speed on the different computation paths depends on the choices of a scheduler. We show that finite-state model checking of HyperATL* is decidable and present a model checking algorithm based on alternating automata. We establish that our algorithm is asymptotically optimal by proving matching lower bounds. We have implemented a prototype model checker for a fragment of HyperATL* that can check various security properties in small finite-state systems.

Signal Temporal Logic is a linear-time temporal logic designed for classifying the time-dependent signals originating from continuous-state or hybrid-state dynamical systems according to formal specifications. It has been conceived as a tool for systematizing the monitoring of cyber-physical systems, supporting the automatic translation of complex safety specifications into monitoring algorithms, faithfully representing their semantics. Almost all algorithms hitherto suggested do, however, assume perfect identity between the sensor readings, informing the monitor about the system state and the actual ground truth. Only recently have Visconti et al. addressed the issue of inexact measurements, taking up the simple model of interval-bounded per-sample error that is unrelated, in the sense of chosen afresh, across samples. We expand their analysis by decomposing the error into an unknown yet fixed offset and an independent per-sample error and show that in this setting, monitoring of temporal properties no longer coincides with collecting Boolean combinations of state predicates evaluated in each time instant over best-possible per-sample state estimates, but can be genuinely more informative in that it infers determinate truth values for monitoring conditions that interval-based evaluation remains inconclusive about. For the model-free as well as for the linear model-based case, we provide optimal evaluation algorithms based on affine arithmetic and SAT modulo theory, solving over linear arithmetic. The resulting algorithms provide conclusive monitoring verdicts in many cases where state estimations inherently remain inconclusive. In their model-based variants, they can simultaneously address the issues of uncertain sensing and partial observation.

Petri games are a multiplayer game model for the automatic synthesis of distributed systems. We compare two fundamentally different approaches for solving Petri games. The symbolic approach decides the existence of a winning strategy via a reduction to a two-player game over a finite graph, which in turn is solved by a fixed point iteration based on binary decision diagrams (BDDs). The bounded synthesis approach encodes the existence of a winning strategy, up to a given bound on the size of the strategy, as a quantified Boolean formula (QBF). In this paper, we report on initial experience with a prototype implementation of the bounded synthesis approach. We compare bounded synthesis to the existing implementation of the symbolic approach in the synthesis tool ADAM. We present experimental results on a collection of benchmarks, including one new benchmark family, modeling manufacturing and workflow scenarios with multiple concurrent processes.

We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new tools that have entered the competition. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions.

Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks.

A fundamental question in system design is to decide how much of the design of one component must be known in order to successfully design another component of the system. We study this question in the setting of reactive synthesis, where one constructs a system implementation from a specification given in temporal logic. In previous work, we have shown that the system can be constructed compositionally, one component at a time, if the specification admits a "dominant" (as explained in Introduction) strategy for each component. In this paper, we generalize the approach to settings where dominant strategies only exist under certain assumptions about the future behavior of the other components. We present an incremental synthesis method based on the automatic construction of such assumptions.

We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.

In this paper we investigate lossy channel games under incomplete information, where two players operate on a finite set of unbounded FIFO channels and one player, representing a system component under consideration operates under incomplete information, while the other player, representing the component's environment is allowed to lose messages from the channels. We argue that these games are a suitable model for synthesis of communication protocols where processes communicate over unreliable channels. We show that in the case of finite message alphabets, games with safety and reachability winning conditions are decidable and finite-state observation-based strategies for the component can be effectively computed. Undecidability for (weak) parity objectives follows from the undecidability of (weak) parity perfect information games where only one player can lose messages.

The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i.e., for systems whose behavior is characterized by the interplay of uncontrolled environment inputs and controlled system outputs. We show that reactive safety is a strictly larger class of properties than standard safety. We provide algorithms for checking if a property, given as a temporal formula or as a word or tree automaton, is a reactive safety property and for translating such properties into safety automata. Based on this construction, the standard verification and synthesis algorithms for safety properties immediately extend to the larger class of reactive safety.

Writing formal specifications for distributed systems is difficult. Even simple consistency requirements often turn out to be unrealizable because of the complicated information flow in the distributed system: not all information is available in every component, and information transmitted from other components may arrive with a delay or not at all, especially in the presence of faults. The problem of checking the distributed realizability of a temporal specification is, in general, undecidable. Semi-algorithms for synthesis, such as bounded synthesis, are only useful in the positive case, where they construct an implementation for a realizable specification, but not in the negative case: if the specification is unrealizable, the search for the implementation never terminates. In this paper, we introduce counterexamples to distributed realizability and present a method for the detection of such counterexamples for specifications given in linear-time temporal logic (LTL). A counterexample consists of a set of paths, each representing a different sequence of inputs from the environment, such that, no matter how the components are implemented, the specification is violated on at least one of these paths. We present a method for finding such counterexamples both for the classic distributed realizability problem and for the fault-tolerant realizability problem. Our method considers, incrementally, larger and larger sets of paths until a counterexample is found. For safety specifications in weakly ordered architectures we obtain a decision procedure, while counterexamples for full LTL and arbitrary architectures may consist of infinitely many paths. Experimental results, obtained with a QBF-based prototype implementation, show that our method finds simple errors very quickly, and even problems with high combinatorial complexity, like the Byzantine Generals' Problem, are tractable.

Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be efficiently parallelized. In addition to the core logic, we consider the extensions of LTL with bounded-future (BLTL) and past-time (LTL+Past) operators. Even though both extensions improve the succinctness of the logic exponentially, path checking remains efficiently parallelizable: Our algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(logDCFL) \subseteq NC.