CONCUR 2005 – Concurrency Theory

This talk tries to distill several years of experience using both model checking and static analysis to find errors in large software systems. We initially thought that the tradeoffs between the two was clear: static analysis was easy but would mainly find shallow bugs, while model checking would require more work but would be strictly better — it would find more errors, the errors would be deeper and the approach would be more powerful. These expectations were often wrong. This talk will describe some of the sharper tradeoffs between the two, as well as a detailed discussion of one domain — finding errors in file systems code — where model checking seems to work very well.

Regular languages have robust theoretical foundations leading to numerous applications including model checking. Context-free languages and pushdown automata have been indispensable in program analysis due to their ability to model control flow in procedural languages, but the corresponding theory is fragile. In particular, non-closure under intersection and undecidability of the language inclusion problem disallows context-free specifications in model checking applications.

We propose a compositional approach to the dynamics of gene regulatory networks based on the stochastic

π

-calculus, and develop a representation of gene network elements which can be used to build complex circuits in a transparent and efficient way. To demonstrate the power of the approach we apply it to several artificial networks, such as the repressilator and combinatorial gene circuits first studied in Combinatorial Synthesis of Genetic Networks [GEHL2002]. For two examples of the latter systems, we point out how the topology of the circuits and the interplay of the stochastic gate interactions influence the circuit behavior. Our approach may be useful for the testing of biological mechanisms proposed to explain the experimentally observed circuit dynamics.

Joint work with Ralf Blossey and Andrew Phillips.

Games were used by Wittgenstein as an example in the philosophy of language of a concept that can have many and dramatically divergent meanings in different contexts.

Case in point: Games are familiar in the Concurrency community as models of dynamic, multi-staged threats to correctness. In Economics, on the other hand, games refer to a family of mathematical models (including, strictly speaking, the games alluded to above) whose intention is to model the behavior of rational, selfish agents in the face of situations that are to varying degrees competitive and cooperative. In recent years there has been an increasingly active interface, motivated by the advent of the Internet, between the theory of games on the one hand, and the theory of algorithms and complexity on the other, and both with networking. This corpus of research problems and reults is already quite extensive, rich, and diverse; however, one can identify in it at least three salient themes: First, there is the endeavor of developing efficient algorithms for the fundamental computational problems associated with games, such as finding Nash and other equilibria; this quest is more than the predictable reflex of our research community, but it is arguably of fundamental value to Game Theory at large. There is also the field of algorithmic mechanism design, striving to devise computationally efficient methods for designing games whose equilibria are precisely the socially desirable outcomes (for example, that the person who has the highest personal appreciation for the item being auctioned actually wins the auction). And finally we have an ever-expanding family of problems collectively given the playful name “the price of anarchy,” studying how much worse a system emerging from the spontaneous interaction of a group of selfish agents can be when compared with the ideal optimum design.

This talk will review recent results and open problems in these areas.

We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concurrent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their different computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus.

We consider an extension of Lafont’s Interaction Nets, called Multiport Interaction Nets, and show that they are a model of concurrent computation by encoding the full

π

-calculus in them. We thus obtain a faithful graphical representation of the

π

-calculus in which every reduction step is decomposed in fully local graph-rewriting rules.

Model checking for transition systems specified in

π

-calculus has been a difficult problem due to the infinite-branching nature of input prefix, name-restriction and scope extrusion. We propose here an approach to model checking for

π

-calculus by encoding it into a logic which supports reasoning about bindings and fixed points. This logic, called

FOλ

Δ ∇ 

, is a conservative extension of Church’s Simple Theory of Types with a “generic” quantifier. By encoding judgments about transitions in pi-calculus into this logic, various conditions on the scoping of names and restrictions on name instantiations are captured naturally by the quantification theory of the logic. Moreover, standard implementation techniques for (higher-order) logic programming are applicable for implementing proof search for this logic, as illustrated in a prototype implementation discussed in this paper. The use of logic variables and eigenvariables in the implementation allows for exploring the state space of processes in a symbolic way. Compositionality of properties of the transitions is a simple consequence of the meta theory of the logic (i.e., cut elimination). We illustrate the benefits of specifying systems in this logic by studying several specifications of modal logics for pi-calculus. These specifications are also executable directly in the prototype implementation of

FOλ

Δ ∇ 

.

This paper studies the denotational semantics of the typed asynchronous

π

-calculus. We describe a simple game semantics of this language, placing it within a rich hierarchy of games models for programming languages,

A key element of our account is the identification of suitable categorical structures for describing the interpretation of types and terms at an abstract level. It is based on the notion of

closed Freyd category

, establishing a connection between our semantics, and that of the

λ

-calculus. This structure is also used to define a

trace operator

, with which name binding is interpreted. We then show that our categorical characterization is sufficient to prove a weak soundness result.

Another theme of the paper is the correspondence between justified sequences, on which our model is based, and traces in a labelled transition system in which only bound names are passed. We show that the denotations of processes are equivalent, via this correspondence, to their sets of traces. These results are used to show that the games model is fully abstract with respect to may-equivalence.

In this paper, we propose the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties

The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.

Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.

In this paper we use the timed modal logic

L

v

to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (

$L^{cont}_v$

) of the logic

L

v

with a new modality.

More precisely we define a fragment of

L

v

, namely

$L^{det}_v$

, such that any control objective of

$L^{det}_v$

can be translated into a

$L^{cont}_v$

formula that holds for the plant if and only if there is a controller that can enforce the control objective.

We also show that the new modality of

$L^{cont}_v$

strictly increases the expressive power of

L

v

while model-checking of

$L^{cont}_v$

remains EXPTIME-complete.

We show that stopwatch automata are equivalent to timed shuffle expressions, an extension of timed regular expressions with the shuffle operation. This implies that the emptiness problem for timed shuffle expressions is undecidable. The result holds for both timed state sequence semantics and timed event sequence semantics of automata and expressions.

Similarly to timed regular expressions, our timed shuffle expressions employ renaming. But we show that even when renaming is not used, shuffle regular expressions still have an undecidable emptiness problem. This solves in the negative a conjecture of Asarin on the possibility to use shuffle to define timed regular languages.

The context of this study is timed temporal logics for timed automata. In this paper, we propose an extension of the classical logic

TCTL

with a new Until modality, called “Until almost everywhere”. In the extended logic, it is possible, for instance, to express that a property is true at all positions of all runs, except on a negligible set of positions. Such properties are very convenient, for example in the framework of boolean program verification, where transitions result from changing variable values. We investigate the expressive power of this modality and in particular, we prove that it cannot be expressed with classical

TCTL

modalities. However, we show that model-checking the extended logic remains PSPACE-complete as for

TCTL

.

Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.

Metric labelled transition systems are labelled transition systems whose states and actions form (pseudo)metric spaces. These systems can capture a large class of timed transition systems, including systems with uncountably many states and uncountable nondeterminism. In this paper a behavioural pseudometric is introduced for metric labelled transition systems. The behavioural distance between states, a nonnegative real number, captures the similarity of the behaviour of those states. The smaller the distance, the more alike the states are. In particular, the distance between states is 0 iff they are bisimilar. Three different characterisations of this pseudometric are given: a fixed point, a logical and a coinductive characterisation. These generalise the fixed point, logical and coinductive characterisations of bisimilarity.

We study notions of

equivalence

and

refinement

for probabilistic programs formalized in the second-order fragment of Probabilistic Idealized Algol. Probabilistic programs implement randomized algorithms: a given input yields a probability distribution on the set of possible outputs. Intuitively, two programs are equivalent if they give rise to identical distributions for all inputs. We show that equivalence is decidable by studying the fully abstract game semantics of probabilistic programs and relating it to probabilistic finite automata. For terms in

β

-normal form our decision procedure runs in time exponential in the syntactic size of programs; it is moreover fully compositional in that it can handle

open

programs (probabilistic modules with unspecified components).

In contrast, we show that the natural notion of program refinement, in which the input-output distributions of one program uniformly dominate those of the other program, is undecidable.

The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending mails. The systems for ensuring anonymity often use random mechanisms which can be described probabilistically, while the agents’ interest in performing the anonymous action may be totally unpredictable, irregular, and hence expressable only nondeterministically.

Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which both the systems and the user can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users.

We formulate our notions of anonymity in terms of observables for processes in the probabilistic

π

-calculus, whose semantics is based on Probabilistic Automata.

We illustrate our ideas by using the example of the dining cryptographers.

A realistic threat model for cryptographic protocols or for language-based security should include a dynamically growing population of principals (or security levels), some of which may be compromised, that is, come under the control of the adversary. We explore such a threat model within a pi-calculus. A new process construct records the ordering between security levels, including the possibility of compromise. Another expresses the expectation of conditional secrecy of a message—that a particular message is unknown to the adversary unless particular levels are compromised. Our main technical contribution is the first system of secrecy types for a process calculus to support multiple, dynamically-generated security levels, together with the controlled compromise or downgrading of security levels. A series of examples illustrates the effectiveness of the type system in proving secrecy of messages, including dynamically-generated messages. It also demonstrates the improvement over prior work obtained by including a security ordering in the type system. Perhaps surprisingly, the soundness proof for our type system for symbolic cryptography is via a simple translation into a core typed pi-calculus, with no need to take symbolic cryptography as primitive.

We present a discretely timed spi-calculus. A primitive for key compromise allows us to model key compromise attacks, thus going beyond the standard Dolev-Yao attacker model. A primitive for reading a global clock allows us to express protocols based on timestamps, which are common in practice. We accompany the timed spi-calculus with a type system, prove that well-typed protocols are robustly safe for secrecy and authenticity and present examples of well-typed protocols as well as an example where failure to typecheck reveals a (well-known) flaw.

Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for

recursive

protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear left-hand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability.

In this paper, we propose a formalism, called

selecting theories

, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in

nexptime

.

Research on the automatic analysis of cryptographic protocols has so far mainly concentrated on reachability properties, such as secrecy and authentication. Only recently it was shown that certain game-theoretic security properties, such as balance for contract-signing protocols, are decidable in a Dolev-Yao style model with a bounded number of sessions but unbounded message size. However, this result does not provide a practical algorithm as it merely bounds the size of attacks. In this paper, we prove that game-theoretic security properties can be decided based on standard constraint solving procedures. In the past, these procedures have successfully been employed in implementations and tools for reachability properties. Our results thus pave the way for extending these tools and implementations to deal with game-theoretic security properties.

We consider a generic process algebra of which the standard process algebras ACP, CCS and CSP are subalgebras of reduced expressions. In particular such an algebra is endowed with a recursion operator which computes minimal fixpoint solutions of systems of equations over processes. As model for processes we consider finite-state transition systems modulo Milner‘s observational congruence and we define an operational semantics for the process algebra. Over such a generic algebra we show the following. We provide a syntactical characterization (allowing as many terms as possible) for the equations involved in recursion operators, which guarantees that transition systems generated by the operational semantics are indeed finite-state. Vice-versa we show that every process admits a specification in terms of such a restricted form of recursion. We then present an axiomatization which is ground-complete over such a restricted signature: an equation can be derived from the axioms between closed terms exactly when the corresponding finite-state transition systems are observationally congruent. Notably, in presenting such an axiomatization, we also show that the two standard axioms of Milner for weakly unguarded recursion can be expressed by using just a single axiom.

We propose a polynomial-time decision procedure for hereditary history preserving bisimilarity (hhp-b) on Basic Parallel Processes (BPP). Furthermore, we give a sound and complete equational axiomatization for the equivalence. Both results are derived from a decomposition property of hhp-b, which is the main technical contribution of the paper. Altogether, our results complement previous work on complexity and decomposition of classical and history-preserving bisimilarity on BPP.

Coinductive definitions of semantics based on bisimulations have rather pleasant properties and are simple to use. In order to get coinductive characterisations of those semantic equivalences that are weaker than strong bisimulation we use a variant of the bisimulation up-to technique in which we allow the use of a given preorder relation. We prove that under some technical conditions our bisimulations up-to characterise the kernel of the given preorder. It is remarkable that the adequate orientation of the ordering relation is crucial to get this result. As a corollary, we get nice coinductive characterisations of all the axiomatic semantic equivalences in Van Glabbeek’s spectrum. Although we first prove our results for finite processes, reasoning by induction, then we see, by using continuity arguments, that they are also valid for infinite (finitary) processes.

The focus of process calculi is

interaction

rather than

computation

, and for this very reason: (i) their operational semantics is conveniently expressed by labelled transition systems (LTSs) whose labels model the possible interactions with the environment; (ii) their abstract semantics is conveniently expressed by observational congruences. However, many current-day process calculi are more easily equipped with reduction semantics, where the notion of

observable action

is missing. Recent techniques attempted to bridge this gap by synthesising LTSs whose labels are process contexts that enable reactions and for which bisimulation is a congruence. Starting from Sewell’s set-theoretic construction, category-theoretic techniques were defined and based on Leifer and Milner’s

relative pushouts

, later refined by Sassone and the fourth author to deal with structural congruences given as

groupoidal 2-categories

.

Building on recent works concerning observational equivalences for

tile logic

, the paper demonstrates that

double categories

provide an elegant setting in which the aforementioned contributions can be studied. Moreover, the formalism allows for a straightforward and natural definition of weak observational congruence.

We lay the foundations for a Structural Operational Semantics (SOS) framework for higher order processes. Then, we propose a number of extensions to Bernstein’s

promoted tyft/tyxt

format which aims at proving congruence of strong bisimilarity for higher order processes. The extended format is called

promoted PANTH

. This format is easier to apply and strictly more expressive than the

promoted tyft/tyxt

format. Furthermore, we propose and prove a congruence format for a notion of

higher order bisimilarity

arising naturally from our SOS framework. To illustrate our formats, we apply them to Thomsen’s Calculus of Higher Order Communicating Systems (CHOCS).

Starting from the opinion that the standard firing rule of Petri nets embodies the collective token interpretation of nets rather than their individual token interpretation, I propose a new firing rule that embodies the latter. Also variants of both firing rules for the self-sequential interpretation of nets are studied. Using these rules, I express the four computational interpretations of Petri nets by semantic mappings from nets to labelled step transition systems, the latter being event-oriented representations of higher dimensional automata. This paper totally orders the expressive power of the four interpretations, measured in terms of the classes of labelled step transition systems up to isomorphism of reachable parts that can be denoted by nets under each of the interpretations. Furthermore, I extend the unfolding construction of place/transition nets into occurrence net to nets that may have transitions without incoming arcs.

Model checking based on Petri net unfoldings is an approach widely applied to cope with the state space explosion problem.

In this paper we propose a new condensed representation of a Petri net’s behaviour called

merged processes

, which copes well not only with concurrency, but also with other sources of state space explosion, viz. sequences of choices and non-safeness. Moreover, this representation is sufficiently similar to the traditional unfoldings, so that a large body of results developed for the latter can be re-used. Experimental results indicate that the proposed representation of a Petri net’s behaviour alleviates the state space explosion problem to a significant degree and is suitable for model checking.

We present the concurrency and distribution primitives of

X10

, a modern, statically typed, class-based object-oriented (OO) programming language, designed for high productivity programming of scalable applications on high-end machines. The basic move in the

X10

programming model is to reify locality through a notion of

place

, which hosts multiple data items and activities that operate on them. Aggregate objects (such as arrays) may be distributed across multiple places. Activities may dynamically spawn new activities in mulitple places and sequence them through a

finish

operation that detects termination of activities. Atomicity is obtained through the use of

atomic blocks

. Activities may repeatedly detect quiescence of a data-dependent collection of (distributed) activities through a notion of

clocks

, generalizing barriers. Thus

X10

has a handful of orthogonal constructs for

space

,

time

,

sequencing

and

atomicity

.

X10

smoothly combines and generalizes the current dominant paradigms for shared memory computing and message passing.

We present a bisimulation-based operational semantics for

X10

building on the formal semantics for “Middleweight Java”. We establish the central theorem of

X10

: programs without conditional atomic blocks do not deadlock.

We develop a behavioural theory of distributed programs in the presence of failures such as nodes crashing and links breaking. The framework we use is that of D

π

, a language in which located processes, or agents, may migrate between dynamically created locations. In our extended framework, these processes run on a distributed network, in which individual nodes may crash in fail-stop fashion or the links between these nodes may become permanently broken. The original language, D

π

, is also extended by a ping construct for detecting and reacting to these failures.

We define a bisimulation equivalence between these systems, based on labelled actions which record, in addition to the effect actions have on the processes, the effect on the actual state of the underlying network and the view of this state known to observers. We prove that the equivalence is

fully abstract

, in the sense that two systems will be differentiated if and only if, in some sense, there is a computational context, consisting of a surrounding network and an observer, which can see the difference.

Web services composition is an emerging paradigm for the integration of long running business processes, attracting the interest of both Industry, in terms of XML-based standards for business description, and Academy, exploiting process description languages. The key challenging aspects to model are orchestration workflows, choreography of exchanged messages, fault handling, and transactional integrity with compensation mechanisms. Few recent proposals attempted to mitigate the explosion of XML-constructs in ad hoc standards by a careful selection of a small set of primitives related to the above aspects. This papers clarifies analogies and differences between two such recent process description languages: one based on interleaving trace semantics and the other on concurrent traces. We take advantage of their comparison to characterise and relate four different coordination policies for compensating parallel processes. Such policies differ on the way in which the abort of a process influences the execution of sibling processes, and whether compensation is distributed or centralised.

We propose a formalisation of the notion of transaction, using a variant of CCS, RCCS, that distinguishes reversible and irreversible actions, and incorporates a distributed backtrack mechanism. Any weakly correct implementation of a transaction in CCS, once embedded in RCCS, automatically obtains a correct one. We show examples where this method allows for a more concise implementation and a simpler proof of correctness.

We study infinite stochastic games played by two-players on a finite graph with goals specified by sets of infinite traces. The games are

concurrent

(each player simultaneously and independently chooses an action at each round),

stochastic

(the next state is determined by a probability distribution depending on the current state and the chosen actions),

infinite

(the game continues for an infinite number of rounds),

nonzero-sum

(the players’ goals are not necessarily conflicting), and undiscounted. We show that if each player has an

ω

-regular objective expressed as a parity objective, then there exists an

ε

-Nash equilibrium, for every

ε

> 0. However, exact Nash equilibria need not exist. We study the complexity of finding values (payoff profile) of an

ε

-Nash equilibrium. We show that the values of an

ε

-Nash equilibrium in nonzero-sum concurrent parity games can be computed by solving the following two simpler problems: computing the values of zero-sum (the goals of the players are strictly conflicting) concurrent parity games and computing

ε

-Nash equilibrium values of nonzero-sum concurrent games with reachability objectives. As a consequence we establish that values of an

ε

-Nash equilibrium can be computed in TFNP (total functional NP), and hence in EXPTIME.

Reactive systems are often modelled as two person antagonistic games where one player represents the system while his adversary represents the environment. Undoubtedly, the most popular games in this context are parity games and their cousins (Rabin, Streett and Muller games). Recently however also games with other types of payments, like discounted or mean-payoff [5,6], previously used only in economic context, entered into the area of system modelling and verification. The most outstanding property of parity, mean-payoff and discounted games is the existence of optimal positional (memoryless) strategies for both players. This observation raises two questions: (1) can we characterise the family of payoff mappings for which there always exist optimal positional strategies for both players and (2) are there other payoff mappings with practical or theoretical interest and admitting optimal positional strategies. This paper provides a complete answer to the first question by presenting a simple necessary and sufficient condition on payoff mapping guaranteeing the existence of optimal positional strategies. As a corollary to this result we show the following remarkable property of payoff mappings: if both players have optimal positional strategies when playing solitary one-player games then also they have optimal positional strategies for two-player games.

The classical modelization of concurrent system behaviors is based on observing execution sequences of global states. This model is intuitively simple and enjoys a variety of mathematical tools, e.g. finite automata, helping verifying concurrent systems. On the other hand, parallel composition of local controllers are needed when dealing with the actual implementation of concurrent models. A well known tool for turning global observation into local controllers is Zielonka’s theorem, and its derivatives. We give here another algorithm, simpler and cheaper than Zielonka’s theorem, in the case where the events observed do not include communication but only local asynchronous actions. In a developer point of view, it means that she does not have to explicitly specify the messages needed, which will be added (if allowed) automatically by the implementation algorithm.

We propose a definition for the class of all fairness properties of a given system. We provide independent characterizations in terms of topology, language theory and game theory. All popular notions of fairness from the literature satisfy our definition. Moreover our class is closed under union and countable intersection, and it is, in a sense, the maximal class having this property. On the way, we characterize a class of liveness properties, called

constructive liveness

, which is interesting by itself because it is also closed under union and countable intersection. Furthermore, we characterize some subclasses of liveness that are closed under arbitrary intersection.

We introduce two abstract models for multithreaded programs based on dynamic networks of pushdown systems.We address the problem of symbolic reachability analysis for these models. More precisely, we consider the problem of computing effective representations of their reachability sets using finite-state automata. We show that, while forward reachability sets are not regular in general, backward reachability sets starting from regular sets of configurations are always regular. We provide algorithms for computing backward reachability sets using word/tree automata, and show how these algorithms can be applied for flow analysis of multithreaded programs.

Usually, ranking function synthesis and invariant generation over a loop with integer variables involves abstracting the loop to have real variables. Integer division and modulo arithmetic must be soundly abstracted away so that the analysis over the abstracted loop is sound for the original loop. Consequently, the analysis loses precision. In contrast, we introduce a technique for handling loops over integer variables directly. The resulting analysis is more precise than previous analyses.

In this paper we show how to compress efficiently the state-space of a concurrent system (here applied to a simple shared memory model, but this is no way limited to that model). The technology used here is based on research on geometric semantics by the authors and collaborators [1]. It has been implemented in a abstract interpretation based static analyzer (ALCOOL), and we show some preliminary results and benchmarks.

We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in ℤ. The constraint language includes periodicity constraints, comparison constraints of the form

x

=

y

and

x

<

y

, it is closed under Boolean operations and it admits a restricted form of existential quantification. This is the largest set of qualitative constraints over ℤ known so far, shown to admit a decidable LTL extension. Such constraints are those used for instance in calendar formalisms or in abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. As a by-product, LTL model-checking over integral relational automata is proved complete for polynomial space which contrasts with the known undecidability of its CTL counterpart.

We continue our study of the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In a previous paper (CONCUR 2003), we investigated the class of local and MSO definable temporal logics that capture all known temporal logics and we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed). In this paper, we concentrate on the uniform satisfiability problem: we consider the dependence alphabet (i.e., the architecture of the distributed system) as part of the input. We prove lower and upper bounds for the uniform satisfiability problem that depend on the number of monadic quantifier alternations present in the chosen MSO-modalities.

Software is often being assembled using third-party components where the developers have little knowledge of, and even less control over, the internals of the components comprising the overall system. One obstacle to composing agents is that current formal methods are mainly concerned with “closed” systems that are built from the ground up. Such systems are fully under the control of the user. Hence, problems arising from ill-specified components can be resolved by a close inspection of the systems. When composing systems using “off-the-shelf” components, this is often no longer the case.

The paper addresses the problem of

under-specification

, where an off-the-shelf component does only what it claims to do, however, it claims more behaviors than it actually has and that one wishes for, some of which may render it useless. Given such an under-specified module, we propose a method to automatically synthesize some safety properties from it that would tame its “bad” behaviors. The advantage of restricting to safety properties is that they are monitorable.

The safety properties are derived using an automata-theoretic approach. We show that, when restricting to

ω

-regular languages, there is no maximal safety property. For this case we construct a sequence of increasingly larger safety properties. We also show how to construct an infinite-state automata that can capture any safety property that is contained in the original specifications.

We consider the problem of synthesizing protocols in a distributed setting satisfying specifications phrased in the logic of linear time

and

knowledge. On the one hand, we show that synthesis is already undecidable in environments with just two agents, one of which observes every aspect of the system state and one of which observes nothing of it. This falsifies a conjecture of van der Meyden and Vardi from CONCUR’96. On the other hand, we prove that synthesis is decidable in broadcast environments, verifying a conjecture of van der Meyden and Vardi from the same paper, and we show that for specifications that are positive in the knowledge modalities the synthesis problem can be reduced to the same problem for formulas without knowledge modalities. After adapting Pnueli and Rosner’s decidability result on synthesis for linear temporal logic specifications in hierarchical environments, we obtain that, in our setting, synthesis is decidable for specifications positive in the knowledge modalities when restricted to hierarchical environments. We conclude the decidability in hierarchical systems of a property closely related to nondeducibility on strategies, a notion that has been studied in computer security.