CONCUR 2015 ACCEPTED PAPERS

(with Abstracts)

C. Aiswarya, Benedikt Bollig and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms

Abstract: We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.

Sergueï Lenglet and Alan Schmitt. Howe's Method for Contextual Semantics

Abstract: We show how to use Howe's method to prove that context bisimilarity is a congruence for process calculi equipped with their usual semantics. We apply the method to two extensions of HOpi, with passivation and with join patterns, illustrating different proof techniques.

Dimitrios Kouzapas, Jorge A. Pérez and Nobuko Yoshida. Characteristic Bisimulations for Higher-Order Session Processes

Abstract: Characterising contextual equivalence is a long-standing issue for higher-order (process) languages. In the setting of a higher-order pi-calculus with sessions, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind.

Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes.

We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.

Salvatore La Torre, Anca Muscholl and Igor Walukiewicz. Safety of parametrized asynchronous shared-memory systems is almost always decidable

Abstract: Verification of concurrent systems is a difficult problem in general, and this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague’s setting are pushdown automata. Here, we extend it by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets or multi-pushdown systems with decidable reachability problem.

Marco Carbone, Fabrizio Montesi, Nobuko Yoshida and Carsten Schurmann. Multiparty Session Types as Coherence Proofs

Abstract: This paper proposes a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications in multiparty sessions. The key contribution of our development is generalising the standard notion of duality found in CLL to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle for compositionality of communications, we generalise the standard cut rule of CLL to a new rule for composing multiple processes communicating in the same multiparty session. We finally prove the soundness of our development by showing that our rule for process composition is admissible. As a consequence of this Curry-Howard correspondence, communications among composed processes can always progress.

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas and Tjark Weber. Modal Logics for Nominal Transition Systems

Abstract: We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. We show how to treat different variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.

Laura Bocchi, Julien Lange and Nobuko Yoshida. Meeting Deadlines Together

Abstract: This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory.

Paul Hunter, Guillermo Perez and Jean-Francois Raskin. Reactive Synthesis Without Regret

Abstract: Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. We also establish relations between the latter version and other problems studied in the literature.

David Harel, Guy Katz, Robby Lampert, Assaf Marron and Gera Weiss. On the Succinctness of Idioms for Concurrent Programming

Abstract: The ability to create succinct programs is a central criterion for comparing programming and specification methods. Specifically, approaches to concurrent programming can often be thought of as idioms for the composition of automata, and as such they can then be compared using the standard and natural measure for the complexity of automata, descriptive succinctness. This measure captures the size of the automata that the evaluated approach needs for expressing the languages under discussion. The significance of this metric lies, among other things, in its impact on software reliability, maintainability, reusability and simplicity, and on software analysis and verification. Here, we focus on the succinctness afforded by three basic concurrent programming idioms: requesting events, blocking events and waiting for events. We show that a programming model containing all three idioms is exponentially more succinct than non-parallel automata, and that its succinctness is additive to that of classical nondeterministic and “and” automata. We also show that our model is strictly contained in the model of cooperating automata a la statecharts, but that it may provide similar exponential succinctness over non-parallel automata as the more general model — while affording increased encapsulation. We then investigate the contribution of each of the three idioms to the descriptive succinctness of the model as a whole, and show that they each have their unique succinctness advantages that are not subsumed by their counterparts. Our results contribute to a rigorous basis for assessing the complexity of specifying, developing and maintaining complex concurrent software.

Cesar Rodriguez, Marcelo Sousa, Subodh Sharma and Daniel Kroening. Unfolding-based Partial Order Reduction

Abstract: Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to profit from their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore up to exponentially less, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state-caching. Over, e.g., benchmarks with busy-waits, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.

Shaull Almagor, Guy Avni and Orna Kupferman. Repairing Multi-Player Games

Abstract: Synthesis is the automated construction of systems from their specifications. Modern systems often consist of interacting components, each having its own objective. The interaction among the components is modeled by a {\em multi-player game}. Strategies of the components induce a trace in the game, and the objective of each component is to force the game into a trace that satisfies its specification. This is modeled by augmenting the game with $\omega$-regular winning conditions. Unlike traditional synthesis games, which are zero-sum, here the objectives of the components do not necessarily contradict each other. Accordingly, typical questions about these games concern their stability --- whether the players reach an equilibrium, and their social welfare --- maximizing the set of (possibly weighted) specifications that are satisfied.

We introduce and study {\em repair} of multi-player games. Given a game, we study the possibility of modifying the objectives of the players in order to obtain stability or to improve the social welfare. Specifically, we solve the problem of modifying the winning conditions in a given concurrent multi-player game in a way that guarantees the existence of a {\em Nash equilibrium}. Each modification has a value, reflecting both the cost of strengthening or weakening the underlying specifications, as well as the benefit of satisfying specifications in the obtained equilibrium. We seek optimal modifications, and we study the problem for various $\omega$-regular objectives and various cost and benefit functions. We analyze the complexity of the problem in the general setting as well as in one with a fixed number of players. We also study two additional types of repair, namely redirection of transitions and control of a subset of the players.

Fu Song. On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference

Abstract: Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems by associating each transition rule with a transduction. The associated transductions allow to inspect and modify the stack content at each step of a transition rule. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations $pre^*(C)$ of a regular set $C$ of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute $pre^*(C)$ for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations $post^*(C)$ of a regular set $C$ of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute $pre^*(C)$ and $post^*(C)$. Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.

Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks

Abstract: We present two quantitative behavioral equivalences over species of a chemical reaction network (CRN) with semantics based on ordinary differential equations. Forward CRN bisimulation identifies a partition where each equivalence class represents the exact sum of the concentrations of the species belonging to that class. Backward CRN bisimulation relates species that have the identical solutions at all time points when starting from the same initial conditions. Both notions can be checked using only CRN syntactical information, i.e., by inspection of the set of reactions. We provide a unified algorithm that computes the coarsest refinement up to our bisimulations in polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisimulation. As an application, we find significant reductions in a number of models of biological processes from the literature. In two cases we allow the analysis of benchmark models which would be otherwise intractable due to their memory requirements.

Andrea Cerone, Giovanni Bernardi and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility

Abstract: Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.

Eike Best and Raymond Devillers. Synthesis of Bounded Choice-Free Petri Nets

Abstract: This paper describes a synthesis algorithm tailored to the construction of choice-free Petri nets from finite persistent transition systems. With this goal in mind, a minimised set of simplified systems of linear inequalities is distilled from a general region-theoretic approach. This leads to algorithmic improvements as well as to a partial characterisation of the class of persistent transition systems that have a choice-free Petri net realisation.

Yuan Feng and Mingsheng Ying. Toward automatic verification of quantum cryptographic protocols

Abstract: Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security is obviously guaranteed, with at most an exponentially decreasing gap.

Sadegh Soudjani, Rupak Majumdar and Alessandro Abate. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

Abstract: We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, and run out of memory quickly.

We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.

Julian Gutierrez, Paul Harrenstein and Michael Wooldridge. Expressiveness and Complexity Results for Strategic Reasoning

Abstract: In this paper, we present a range of new expressiveness and complexity results for the specification, computation, and verification of Nash equilibria in multi-player non-zero-sum concurrent games in which players have goals expressed as temporal logic formulae. Our results are based on a new approach to the characterisation of equilibria in such games: a semantic characterisation based on winning strategies and memoryful reasoning. This characterisation allows us to obtain a number of other results relating to the representation of equilibrium properties in temporal logic. In particular, we show that Nash equilibrium can be expressed in ATL$^*$, that constructing strategy profiles in such games can be done in 2EXPTIME using finite-memory strategies, and that in simpler cases (two-player games and sequential games) the specification of equilibria can be obtained in a temporal logic even weaker than ATL$^*$. Based on these results, the paper settles a number of open problems in the literature, puts forward a new logical characterisation of equilibria, and provides either improved answers or alternative solutions to a number of questions.

Taolue Chen, Fu Song and Zhilin Wu. On the Satisfiability of Indexed Linear Temporal Logics

Abstract: Indexed Linear Temporal Logics (ILTL) are an extension of standard Linear Temporal Logics (LTL) with quantifications over index variables which range over a set of process identifiers. ILTL has been widely used in specifying and verifying properties of parameterised systems, e.g., in parameterised model checking of concurrent processes. However there is still a lack of theoretical investigations on properties of ILTL, compared to the well-studied LTL. In this paper, we start to narrow this gap, focusing on the satisfiability problem, i.e., to decide whether a model exists for a given formula. This problem is in general undecidable. Various fragments of ILTL have been considered in the literature typically in parameterised model checking, e.g., ILTL formulae in prenex normal form, or containing only non-nested quantifiers, or admitting limited temporal operators. We carry out a thorough study on the decidability and complexity of the satisfiability problem for these fragments. Namely, for each fragment, we either show that it is undecidable, or otherwise provide tight complexity bounds.

Patricia Bouyer, Samy Jaziri and Nicolas Markey. On the Value Problem in Weighted Timed Games

Abstract: A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been identified for which optimal cost and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in weighted timed games. We then introduce a large subclass of weighted timed games (for which the undecidability proof above applies), and provide an algorithm to compute arbitrary approximations of the value in such games. To the best of our knowledge, this is the first approximation scheme for an undecidable class of weighted timed automata.

Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by continuous operators

Abstract: Compositional reasoning over probabilistic systems wrt. behavioral metric semantics requires that the language operators are uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators.

Yuxin Deng, Yuan Feng and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi

Abstract: In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear con- texts, where programs are used or executed once, will be more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution- based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.

Dana Fisman and Yoad Lustig. A Modular Approach for Büchi Determinization

Abstract: The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal B\"uchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition. While some improvements were published since the Safra construction, notably Kähler and Wilke’s construction, understanding the constructions remains a non-trivial task.

In this paper we present a modular approach to B\"uchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of Kähler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton’s width is one. Then we show how to construct a deterministic automaton in the case the skeleton’s width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs

Abstract: Asynchronous programming has become ubiquitous in smartphone and web application development, but also in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls---procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.

Filippo Bonchi, Daniela Petrisan, Damien Pous and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations

Abstract: Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras.

In this paper, we prove the soundness of up-to contextual closure for weak bisimilations of systems specified by cool rule formats, as defined by van Glabbeek to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax-bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered enriched setting.

David Baelde, Stephanie Delaune and Lucca Hirschi. Partial Order Reduction for Security Protocols

Abstract: Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools.

In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux and Rupak Majumdar. Verification of Population Protocols

Abstract: Population protocols (Angluin et al., 2006) are a formal model of sensor networks consisting of identical mobile devices. When two devices come into the range of each other, they interact and change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint.

A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value.

While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.

Vojtech Forejt and Jan Krcal. On Frequency LTL in Probabilistic Systems

Abstract: We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator G^p expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems.

For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound p to be 1 and negations not to be outside any G^p operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.

Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini and Lijun Zhang. Lazy Probabilistic Model Checking without Determinisation

Abstract: The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Buchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach -- both explicit and symbolic versions -- in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.

Romain Brenguier, Jean-Francois Raskin and Ocan Sankur. Assume-Admissible Synthesis

Abstract: In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule define sets of solutions which are rectangular. This property leads to solutions which are robust and resilient. We provide complete algorithms with optimal complexity and also an abstraction framework which allows us to define necessary conditions to compute compositionally sets of winning assume-admissible strategies for each player in the game.

Jan Kretinsky, Kim G. Larsen, Simon Laursen and Jiri Srba. Polynomial Time Decidability of Weighted Synchronization under Partial Observability

Abstract: We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.

Nathalie Bertrand, Paulin Fournier and Arnaud Sangnier. Distributed local strategies in broadcast networks

Abstract: We study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes follow the same local strategy that, given the past performed action and received messages, provides the next action to be performed. We show that the reachability and target problem under such local strategies are NP-complete, assuming that the set of receivers is chosen non-deterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained with the additional assumption that all processes are bound to receive the broadcast messages.

Thomas Brihaye, Gilles Geeraerts, Axel Haddad and Benjamin Monmege. To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games

Abstract: Quantitative games are two-player zero-sum games played on directed weighted graphs. Total- payoff games--—that can be seen as a refinement of the well-studied mean-payoff games—--are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics allowing one to possibly speed up the computations in both cases.