previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 8: Invited lecture
Sequential Decision Making with Information Asymmetry

ABSTRACT. We survey some recent results in sequential decision making under uncertainty, where there is an information asymmetry among the decision-makers. We consider two versions of the problem: persuasion and mechanism design. In persuasion, a more-informed principal influences the actions of a less-informed agent by signaling information. In mechanism design, a less-informed principal incentivizes a more-informed agent to reveal information by committing to a mechanism, so that the principal can make more informed decisions. We define Markov persuasion processes and Markov mechanism processes that model persuasion and mechanism design into dynamic models. Then we survey results on optimal persuasion and optimal mechanism design on myopic and far-sighted agents. These problems are solvable in polynomial time for myopic agents but hard for far-sighted agents.

10:30-12:00 Session 9: Verification
Regular Model Checking Upside-Down: An Invariant-Based Approach

ABSTRACT. Regular model checking is a well-established technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. It applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the set of reachable configurations.

In this paper we develop a complementary approach. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and compute increasingly smaller regular supersets of it. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since the intersection is in general non-regular, we introduce $b$-bounded invariants, defined as those representable by CNF-formulas with at most $b$ clauses. We prove that, for every $b \geq 0$, the intersection of all $b$-bounded inductive invariants is regular, and show how to construct an automaton recognizing it. Finally, we study the complexity of deciding if this automaton accepts some unsafe configuration. We show that the problem is in \textsc{EXPSPACE} for every $b \geq 0$, and \textsc{PSPACE}-complete for $b=1$. Finally, we study the performance of our approach in a number of benchmarks.

On an Invariance Problem for Parameterized Concurrent Systems
PRESENTER: Lucas Bueri

ABSTRACT. We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called \emph{havoc invariance}, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem $\phi \models \psi$, asking if any model of $\phi$ is also a model of $\psi$. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.

Towards Concurrent Quantitative Separation Logic
PRESENTER: Ira Fesefeldt

ABSTRACT. In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic - Quantitative Separation Logic and Concurrent Separation Logic - into a new separation logic able to reason about lower bounds of the probability to realize a postcondition after executing such a program.

14:00-15:30 Session 10: Languages & logics
Completeness Theorems for Kleene Algebra with Top

ABSTRACT. We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant 'top' for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events.

Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties

ABSTRACT. Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S(E) of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL, we establish a characterization of the singleton models in terms of the extension of standard FO over traces with addition. This last result generalizes the well-known equivalence between FO and LTL. Finally, we identify new boundaries on the decidability of model checking Context HyperLTL.

Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages

ABSTRACT. One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of `simple' asynchronous automata.

Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest. The proof of its expressive completeness is rather subtle.

Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.

16:00-17:30 Session 11: Test of Time award + Best paper award + Business meeting
Approximate symbolic model checking of continuous-time Markov chains (CONCUR 1999)

ABSTRACT. The paper presented the first symbolic model-checking algorithm for systems that combine probabilistic and real-time behaviors. Specifically, the model-checking algorithm handles real-time probabilistic systems, modeled by continuous-time Markov chains systems, and specifications in CSL -- a branching and continuous-time stochastic logic. This setting significantly extends the scope of systems to which automatic model-checking can be applied. Beyond the new model-checking algorithm, the paper introduces several ideas which have been extensively used since their introduction in the paper. This includes a reduction from a quantitative model-checking problem to the problem of solving a system of equations, as well as a generalization of BDDs, to MTDDs (multi-terminal decision diagrams), which allow both Boolean and real-valued variables, and which enables symbolic reasoning.

The Impressive Power of Stopwatches (CONCUR 2000)

ABSTRACT. The paper studies the expressive power of timed automata enriched with stopwatches and unobservable behaviours. Surprisingly, it is proved with smart constructions that this seemingly mild extension already reaches the full expressive power of linear hybrid automata, a very powerful model using a finite discrete control together with continuous variables, linear guards and linear updates. An important consequence is the reduction of the reachability analysis of linear hybrid automata to that of stopwatch automata. Even though both problems are undecidable, approximate reachability for stopwatch automata is easier to develop and implement. Stopwatch automata find another very important application in the field of scheduling problems for timed pre-emptive systems.

Deriving Bisimulation Congruences for Reactive Systems (CONCUR 2000)

ABSTRACT. The paper presents a uniform approach for deriving a Labelled Transition System (LTS) semantics from a reduction semantics, in such a way that the resulting bisimilarity is a congruence. LTS semantics, inspired by automata theory, specifies the interactive behaviour of systems, while reduction semantics specifies their internal evolution and is closer to the operational semantics of sequential programs. LTS semantics has been favoured in early work on process calculi, as it lends itself to the definition of a variety of behavioural equivalences that are easy to work with. Subsequently, a wealth of process calculi have been proposed, tailored to specific features (mobility, locations, security, sessions, etc). In these more complex calculi, it became more debatable what to adopt as labels or “observables” for the LTS semantics, and this motivated the shift towards a reduction semantics in conjunction with a structural congruence, allowing for a compact semantic description.

The thrust to retrieve an LTS semantics from a reduction semantics is an important one, and this paper is a milestone in this line of work. The solution proposed is robust, i.e., broadly applicable. It is also mathematically elegant, formulated using the categorical notion of relative pushout (RPO). The paper has spurred a whole trend of research on congruence properties for bisimilarity in which RPOs constitute the key notion. Good examples are applications to bigraphs, graph rewriting and name calculi.

The Element of Surprise in Timed Games (CONCUR 2003)

ABSTRACT. The paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. A key contribution of the paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise as they are played "faster", and the definition of natural concepts of winning conditions for the two players -- ensuring that players can win only by playing according to a physically meaningful strategy. This approach provides a clean answer to the problem of time convergence, and the responsibility of the players in it. For this reason, it has since been the basis of numerous works on timed games. The algorithm established in the paper to study omega-regular conditions in this neat model of timed games is also enticing, resorting to mu-calculus on a cleverly enriched structure.