Dietmar Berwanger (LSV, ENS Cachan)
Information tracking in distributed games (Slides: PDF)
Abstract:
The initial paper of Reif on games with imperfect information shows that games for one player against nature can be solved with a power-set construction. Similar in spirit to the determinisation of automata, the procedure represents (an abstraction of) the knowledge that a player has about the play history. Also in this paper, it is shown that the problem of deciding that a coalition of players has a distributed strategy is undecidable in general, essentially because there is an infinite amount of knowledge that players need to keep track of.
In this talk, we propose a construction that keeps track of the information acquired by a player in a game between a coalition of two or more players against the environment. On basis of this, we develop a semi-decision algorithm for deciding whether there exist distributed winning strategies in parity games of imperfect information.
This is joint work with Lukasz Kaiser (Aachen).
Benedikt Bollig (LSV, ENS Cachan)
Realizability of Dynamic MSC Languages (Slides: PDF)
Abstract:
We introduce dynamic communicating automata (DCA), an extension of communicating finite-state machines that allows for dynamic creation of processes. A DCA comes with three types of actions: (1) a new process can be created, (2) a message can be sent to an already existing process, and (3) a message can be received from an existing process. Processes are identified by means of local process variables, whose values can change dynamically during an execution of an automaton and be updated when a message is received. Messages are stored in bidirectional unbounded FIFO channels, which exist between any two created processes. The behavior of a DCA is be described as a set of message sequence charts (MSCs).
We consider the realizability problem for DCA: given a dynamic MSC grammar (a variant of the fork-and-join grammars introduced by Leucker, Madhusudan, and Mukhopadhyay), is there a DCA defining the same set of MSCs? We show that this problem is decidable in doubly exponential time. Moreover, we identify a class of realizable grammars that can be implemented by finite DCA. (This is joint work with Loic Helouet.)
Ahmed Bouajjani (LIAFA, Paris 7)
On the Verification Problem for Weak Memory Models (Slides: PDF)
Abstract:
We address the verification problem of finite-state concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multi-processor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performance-critical system services employing lock-free synchronization, as well as for the correctness of compiler backends that generate code targeted to run on such architectures.
We consider in this paper combinations of three well-known program order relaxations. We consider first the ``write to read'' relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the ``write to write'' relaxation, leading to a model which is essentially PSO (Partial Store Ordering), or (2) the ``read to read/write'' relaxation, or (3) both of them, as it is done in the RMO (Relaxed Memory Ordering) model for instance.
We define abstract operational models for these weak memory models based on state machines with (potentially unbounded) FIFO buffers, and we investigate the decidability of their reachability and their repeated reachability problems.
We prove that the reachability problem is decidable for the TSO model, as well as for its extension with ``write to write'' relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the ``read to read/write'' relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. We show also that the repeated reachability problem is undecidable for all the considered memory models.
This is a joint work with Mohamed-Faouzi Atig, Sebastian Burckhardt, and Madanlal Musuvathi.
Deepak D'Souza (IISc, Bangalore)
On the equivalance of the pointwise and continuous
semantics of First-Order Logic
with linear
constraints
(Slides: PDF)
Abstract:
We consider a first-order logic with linear constraints which can be interpreted naturally in both a pointwise or continuous way over timed words. We show that the two interpretations of this logic coincide in terms of expressiveness. As a consequence it follows that the pointwise and continuous semantics of the timed temporal logic TPTL (with since) also coincide.
Laurent Doyen (LSV, ENS Cachan)
Energy and Mean-payoff Games (Slides: PDF)
Abstract:
We consider two-player games played on a weighted graph with quantitative objective. In an energy game, the weights represent resource consumption and the objective of the game is to maintain the sum of weights always nonnegative. In a mean-payoff game, the objective is to optimize the limit-average usage of the resource.
We use the log-space equivalence between energy games and mean-payoff games to propose a new pseudopolynomial fixpoint algorithm for solving such games, improving the best known worst-case complexity for pseudopolynomial mean-payoff algorithms.
Then, we consider games with imperfect information where the state space is partitioned into classes of indistinguishable states, giving players partial knowledge of the state. We show that the problem of determining if an energy game with imperfect information and fixed initial credit has a winning strategy is decidable, while the question of the existence of some initial credit such that the game has a winning strategy is undecidable. This undecidability result carries over to mean-payoff games with imperfect information.
On the positive side, using a simple restriction on the game graph (namely, that the weights are visible), we show that these problems become EXPTIME-complete.
This talk is based on joint work with Aldric Degorre, Raffaella Gentilini, Jean-Francois Raskin, and Szymon Torunczyk.
Paul Gastin (LSV, ENS Cachan)
Weighted MSO versus Probabilistic Logics (Slides: PDF)
Abstract:
While a mature theory around logics such as MSO, LTL, and CTL has been developed in the pure boolean setting of finite automata, weighted automata lack such a natural connection with (temporal) logic and related verification algorithms. We will identify weighted versions of MSO and CTL that generalize the classical logics and even other quantitative extensions such as probabilistic CTL. We establish expressiveness results on our logics giving translations from weighted and probabilistic CTL into weighted MSO.
Stefan Haar (LSV, ENS Cachan)
Event structure framework for supervising partially observable systems
Abstract:
The partial order view on system semantics allows to cast some classical system control tasks in a more general setting, in which new features and challenges become apparent. To cite one example, fault diagnosis is a classical task in control of discrete event systems (DES). It consists in determining, from a partial observation of the system behaviour, whether or not a given ``invisible'' fault event has occurred. Observability is governed by a partial mapping, the labeling, of transitions to names which can be interpreted as alarm names; the challenge for the observer / supervisor lies in both the presence of invisible (\epsilon-labeled) transitions and the ambiguity of labelling for the visible ones. The problem of diagnosability is: does the labeling allow for an outside observer to determine the occurrence of a given fault, no later than a bounded "time" after that unobservable occurrence ? In previous work, we have proposed an extension of a classical characterization of diagnozability for finite state-machines, given by by Sampath et al. in the 1990s approach to diagnosis in the context of asynchronous system with partial order semantics. Some systems not diagnosable under that interleaved view turn out to be diagnosable in a generalized sense adapted to non-interleaved behaviour of Petri nets. These phenomena motivate a broader view on system properties, formalized in terms of topological properties of prime event structures (PES), in which different semantics represent nonsequential DES behaviour. By selecting adequate pseudometrics on PES, properties such system observability and diagnosability can be translated into topological objects, allowing for novel and unified characterizations that can be separated from the choice of semantics.
The framework is designed to encompass, in the future, other tasks such as active diagnosis or conformance testing.
Loic Helouet (IRISA, Rennes)
Discovering covert channels with information theory (Slides: PDF, PPT, PPTX )
Abstract:
In this work, we investigate how Information Theory can be used to detect illegal flows of information in distributed systems. These flows are usually called covert channels. A covert channel is usually implemented via an obfuscated but legal use of the system by a pair of users that are not allowed to communicate by the security policy of the system. The basic principle of a covert channel is usually to write some information in the system that can be read later.
It has been frequently written in the literature that covert channels are a specific case of non-interference. Two users U and V are said to interfere via a system S if and only if what U does affects what V can see or do. More formally, "affecting what a process can see or do" is characterized as an equivalence relation between behaviors (trace equivalence, bisimulation, …)
We will show in this talk that interference is not sufficient to characterize covert flows of information. Indeed, a covert channel can be seen as a repeated and arbitrary long transfer of information, and two users interfere as soon as they can leak one bit of information during the entire life of the system. We will also show that it is not sufficient either to require repetition of an interference, as each use of a covert channel can transfer less than one bit of information, which is usually not captured by equivalences.
Finally, we will show how information theory can help discovering covert information flows, even when less than one bit of information is passed at each channel use. We will show that discovery of a covert flow can be brought back to a computation of the capacity of a communication channel, and give sufficient conditions such that this capacity computation converges rapidly.
This is joint work with Aline Roumy (INRIA Rennes)
Akash Lal (MSR, Bangalore)
Concurrency and Weighted Automata (Slides: PDF, PPTX)
Abstract:
Weighted automata are finite-state machines in which transitions are additionally labelled with "weights". The weights are elements of some algebraic structure. Depending on the algebraic structure used, the weighted automata can have different properties. While weighted automata have been studied in various contexts, their use for dataflow analysis has been limited. One reason behind this is that algebraic structure used in such a context is a semiring, which has very weak properties. For instance, there is no algorithm for the intersection of weighted automata on semirings.
In this talk, I will present an intersection algorithm for weighted automata, when the weights come from a special subclass of semirings, in particular, ones that have a tensor operation. I will additionally show that there are interesting semirings in this class.
I will also show how this intersection operation leads to new algorithms for the analysis of concurrent programs. When each thread of a concurrent program can be modelled using a Weighted Pushdown System (a general model for multi-procedure programs), and the weights come from a semiring with a tensor operation, then the intersection operation above allows us to solve the problem of context-bounded analysis: i.e., to precisely find the set of behaviours of the concurrent program when the number of context switches allowed in an execution is bounded by a constant.
Kamal Lodaya (IMSc, Chennai)
LTL can be more succinct (Slides: PDF)
Abstract:
It is well known that model checking Linear Temporal Logic (LTL) on finite words is Pspace-complete. Wolper showed that with grammar operators, this result can be extended to increase the expressiveness of the logic to all regular languages. Other ways of extending the expressiveness of LTL using modular and group modalities have been explored by Baziramwabo, McKenzie and Th\'erien, and more recently by Serre, which are expressively complete for regular languages recognized by solvable monoids and for all regular languages, respectively. In all the papers mentioned, the numeric constants used in the modalities are in unary notation. We observe that in some cases (such as the modular modalities) we can use numeric constants in binary notation, and still maintain the Pspace upper bound.
This is joint work with A.V. Sreejith.
Antoine Meyer (Marne-la Vallee)
Counting CTL (Slides: PDF)
Abstract:
We present a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We analyse the expressiveness and succinctness of these logics with respect to CTL and the complexity of their model-checking problem (ranging from P-complete to undecidable).
Joint work with François Laroussinie and Eudes Petonnet.
Joel Ouaknine (Oxford)
On Classical, Real-Time, and Time-Bounded Verification (Slides: PDF)
Abstract:
I will survey the classical, real-time, and time-bounded theories of verification, highlighting key differences and similarities among them, and giving an overview presentation of the solution to a longstanding open problem in the field.
This is joint work with Alex Rabinovich and James Worrell.
Paritosh Pandya (TIFR, Mumbai)
Chop Expressions
Abstract:
We introduce a new variant of extended regular expressions called extended chop expressions with tests (ECET) for specifying epsilon-free regular languages. ECET satisfy the axioms of Boolean Algebras as well as Kleene Algebras with Tests. A complete axiomatisation for equational reasoning about language equality (and containment) of ECET terms is formulated by adapting Kleene's axioms for extended chop expressions. We also investigate the complexities of decision problems such as membership, non-emptiness and non-equivalence for ECET and its subclasses. The algorithmic complexity of synthesis of NFA from extended chop expressions and its subclasses is also investigated. Finally, we formulate the reductions between extended regular expressions and extended chop expressions. Surprisingly, the extended chop expressions seem difficult to reduce to extended regular expressions without considerable blowup in size. Finally, we show equivalence between ECET and DDC*, the discrete duration calculus with chop-star by linear time reductions between them. We also show that equality of KAT algebra expressions of Kozen reduces to equlity of ECET expressions with only polynomial blowup in size. This allows us to use the tool DCVALID for equality of DDC* terms to reason about equlity and containment between a wide variety of expressions including ECET, Regular expressions and KAT algebra terms.
Joint work with Ajesh Babu and Salil Joshi.
Sylvain Salvati (LaBRI, Bordeaux)
Recognizability in the simply typed lambda-calculus
Abstract:
The simply typed lambda-calculus can be seen as a generalization of both strings and trees. As sets of such lambda-terms appear in various contexts, it seems rather natural to bridge the ideas of formal language theory to the study of those sets. As a first step in that direction, we introduce a notion of recognizable sets of simply typed lambda-terms as a generalization of the usual notions of recognizable sets of strings and trees. The main interest of this extension is that it is closed under beta-eta equality which brings computation in the realm of language theory. We will generalize the usual constructions for automata so as to obtain the usual closure properties of recognizable sets under boolean operations and inverse homomorphisms. The closure under inverse homomorphism of recognizable sets of lambda-terms has many interesting applications that are underpinned by the closure of recognizable sets under beta-eta equality. In particular it gives several results about the class of context free languages of lambda-terms and also gives a rather simple proof of decidability of 4th order matching.
Stefan Schwoon (LSV, ENS Cachan)
Unfoldings of contextual Petri nets (Slides: PDF)
Abstract:
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finite-state) Petri nets, which can be used for verification purposes.
Contextual nets are a generalisation of Petri nets suited to model systems with read-only access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan's construction to a suitable encoding of the contextual net into an ordinary net.
However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. We propose a an unfolding algorithm that works for arbitrary semi-weighted, bounded contextual nets.
The talk is based on joint work with Paolo Baldan, Andrea Corradini, and Barbara Koenig.
S P Suresh (CMI, Chennai)
Extensions of Dolev-Yao theory and the secrecy problem (Slides: PDF)
Abstract:
The Dolev-Yao theory has been the mainstay of research in the formal analysis of security protocols, and has formed the basis for a number of protocol verification tools. In the past decade, several extensions of the basic model have been proposed, to handle various additional properties of cryptosystems.
We shall present a brief survey of some of the extensions, and detail some recent work on an extension to handle homomorphic encryption and blind signatures, which is used in some electronic voting protocols. We shall outline the decidability proof of passive intruder deduction for this theory. Interestingly, the proof involves the use of alternating automata.
We end with some remarks on the active intruder theory.
This work is joint with A Baskar (CMI) and R Ramanujam (IMSc).
P S Thiagarajan (NUS, Singapore)
Asynchronous Automata Based Approximations of Distributed Hybrid behaviors (Slides: PDF, PPT)
Abstract:
We consider distributed hybrid automata that observe and control a plant whose state space consists of a finite set of continuous variables evolving at piecewise constant rates. Each automaton in the network can observe a designated subset of the variables and can control a designated subset of the variables. The variables controlled---in terms of effecting mode changes---by different automata are disjoint but the same variable may be observed by more than one automaton. We show that the discrete time behavior of such a network of hybrid automata is regular. More importantly, we show that one can effectively and succinctly represent this regular language as an asynchronous cellular automaton.
This is joint work with Yang Shaofa.
Tayssir Touili (LIAFA, Paris 7)
Reachability Analysis of Networks of Communicating Pushdown Systems
Abstract:
We address the verification problem of networks of communicating pushdown systems modeling communicating parallel programs with procedure calls. Processes in such networks can read the control state of the other processes according to a given communication structure (specifying the observability rights between processes). The reachability problem of such models is undecidable in general. First, we prove that it becomes decidable for networks with acyclic communication structure. Then, we define a class of networks that effectively preserves recognizability (hence, its reachability problem is decidable).
Next, we consider networks where the communication structure can change dynamically during the execution according to a phase graph. The reachability problem for these dynamic networks being undecidable in general, we consider reachability when the switches in the communication structures are bounded. We show that this problem is undecidable even for one switch. Then, we define a natural class of models for which this problem is decidable. This class can be used in the definition of an efficient semi-decision procedure for the analysis of the general model of dynamic networks. Our techniques allowed to find bugs in two versions of a Windows NT Bluetooth driver.
This is joint work with Faouzi Atig and Ahmed Bouajjani.
James Worrell (Oxford)
Reachability in Parametric One-Counter Machines (Slides: PDF)
Abstract:
In this talk we consider one-counter machines in which counter updates can mention integer-valued parameters. Our main result is to show NP-completeness of the problem of determining whether a given state is reachable from the initial state for some value of the parameters. Membership in NP is shown by reduction to the existential fragment of Presburger arithmetic with divisibility.