Search

We consider in the current paper the issue of exploiting the structural form of Esterel programs [BG92] to partition the algorithmic RSS (reachable state space) fix-point construction used in modelchecking techniques [CGP99]. The basic idea sounds utterly simple, as seen on the case of sequential composition: in P;Q, first compute entirely the states reached in P, and then only carry on to Q, each time using only the relevant local transition relation part. Here a brute-force symbolic breadth-first search would have mixed the exploration of P and Q instead. The introduction of parallel (state product) operators, as well as loop iterators and local synchronizing signals make the problem more difficult (and more interesting). We propose techniques to partition statically ("at compile time") the program body, so as to obtain a good trade-off between locality and multiplicity of steps. [ABSTRACT FROM AUTHOR]

The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly. [ABSTRACT FROM AUTHOR]

We provide a treatise about checking proofs of distributed systems by computer using general purpose proof checkers. In particular, we present two approaches to verifying and checking the verification of the Sequential Line Interface Protocol (SLIP), one using rewriting techniques and one using the so-called cones and foci theorem. Finally, we present an overview of literature containing checked proofs. [ABSTRACT FROM AUTHOR]

We recast dataflow in a modern categorical light using profunctors as a generalisation of relations. The well known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve much of the intuitions of a relational model. The development fits with the view of categories of models for concurrency and the general treatment of bisimulation they provide. In particular it fits with the recent categorical formulation of feedback using traced monoidal categories. The payoffs are: (1) explicit relations to existing models and semantics, especially the usual axioms of monotone IO automata are read off from the definition of profunctors, (2) a new definition of bisimulation for dataflow, the proof of the congruence of which benefits from the preservation properties associated with open maps and (3) a treatment of higher-order dataflow as a biproduct, essentially by following the geometry of interaction programme. [ABSTRACT FROM AUTHOR]

Beginning with the category Dom of Scott domains and continuous maps, we introduce a syntax for dataflow networks as "systems of inequalities," and provide an associated operational semantics. We observe that, under this semantics, a system of inequalities determines a two-sided fibration in Dom. This leads to the introduction of a certain class of cartesian arrows of spans as a notion of morphism for systems. The resulting structure Sys, consisting of domains, systems, and morphisms, forms a bicategory that embeds Dom up to equivalence and is suitable as a semantic model for nondeterministic networks. Isomorphism in Sys amounts to a notion of system equivalence "up to deterministic internal computations." [ABSTRACT FROM AUTHOR]

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prefixing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, that agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZ-monad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further investigate structures on Kl(T) that exist for axiomatic reasons, primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi. [ABSTRACT FROM AUTHOR]

We consider the synthesis problem for Elementary Net Systems with Inhibitor Arcs (ENI-systems) executed according to the a-priori semantics. The relationship between nets and transition systems generate by them (TSENI) is established via the notion of a region. The general synthesis problem for ENI-systems was solved in [20], and here we show how to optimise this solution using only minimal regions and selected inhibitor arcs. We also compare the proposed method of eliminating inhibitor arcs in ENI-systems with that introduced in [8] and show that they have similar effect. [ABSTRACT FROM AUTHOR]

The mixed product gives a global representation of concurrent systems modelled by interacting automata. In this paper we study the opposite operation: we characterise the transition systems which may be viewed as products and we build some of their decompositions. For a large subclass of systems, we exhibit a minimal decomposition. We finally extend this study to asynchronous automata whose components may be non-deterministic and present an optimal characterisation of the corresponding transition systems. Thus, we state precisely the shape of the transition systems which are associated to three kinds of system; in that way, we obtain axioms which are similar to those identified for the synthesis problem of Petri nets. [ABSTRACT FROM AUTHOR]

We propose decision procedures based on regions for two problems on pure unbounded Petri nets with injective labelling. One problem is to construct nets from incomplete specifications, given by pairs of regular languages that impose respectively upper and lower bounds on the expected behaviours. The second problem is to derive equivalent nets from deterministic pushdown automata, thus exhibiting their hidden concurrency. [ABSTRACT FROM AUTHOR]

Asynchronous cellular automata and asynchronous automata have been introduced by Zielonka [14] for the study of Mazurkiewicz traces. In [2] Droste & Gastin generalized the first to pomsets. We show that the expressiveness of monadic second order logic and asynchronous cellular automata are different in the class of all pomsets without auto-concurrency. Then we introduce a class where the expressivenesses coincide. This extends the results from [2]. Furthermore, we propose a generalization of trace asynchronous automata for general pomsets. We show that their expressive power coincides with that of monadic second order logic for a large class of pomsets. The universality and the equivalence of asynchronous automata for pomsets are proved to be decidable which is shown to be false for asynchronous cellular automata. [ABSTRACT FROM AUTHOR]

Petri nets with read arcs are investigated w.r.t their unfolding, where read arcs model reading without consuming, which is often more adequate than the destructive-read-and-rewrite modelled with loops in ordinary nets. The paper redefines the concepts of a branching process and unfolding for nets with read arcs and proves that the set of reachable markings of a net is completely represented by its unfolding. The specific feature of branching processes of nets with read arcs is that the notion of a co-set is no longer based only on the binary concurrency relation between the elements of the unfolding, contrary to ordinary nets. It is shown that the existing conditions for finite prefix construction (McMillan's one and its improvement by Esparza et al.) can only be applied for a subclass of nets with read arcs, the so-called read-persistent nets. Though being restrictive, this subclass is sufficiently practical due to its conformance to the notion of hazard-freedom in logic circuits. The latter appear to be one of the most promising applications for nets with read arcs. [ABSTRACT FROM AUTHOR]

In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock synchronization between processes in a network by letting local clocks in each process advance independently of clocks in other processes, and by requiring that two processes resynchronize their local time scales whenever they communicate. A symbolic version of this new semantics is developed in terms of predicate transformers, which enjoys the desired property that two predicate transformers are independent if they correspond to disjoint transitions in different processes. Thus we can apply standard partial order reduction techniques to the problem of checking reachability for timed systems, which avoid exploration of unnecessary interleavings of independent transitions. The price is that we must introduce extra machinery to perform the resynchronization operations on local clocks. Finally, we present a variant of DBM representation of symbolic states in the local time semantics for efficient implementation of our method. [ABSTRACT FROM AUTHOR]

In this paper we solve the following problem: "given a digital circuit composed of gates whose real-valued delays are in an integer-bounded interval, is there a way to discretize time while preserving the qualitative behavior of the circuit?" This problem is described as open in [BS94]. When "preservation of qualitative behavior" is interpreted in a strict sense, as having all original sequences of events with their original ordering we obtain the following two results:1)For acyclic (combinatorial) circuits whose inputs change only once, the answer is positive: there is a constant δ, depending on the maximal number of possible events in the circuit, such that if we restrict all events to take place at multiples of δ, we still preserve qualitative behaviors.2)For cyclic circuits the answer is negative: a simple circuit with three gates can demonstrate a qualitative behavior which cannot be captured by any discretization. Nevertheless we show that a weaker notion of preservation, similar to that of [HMP92], allows in many cases to verify discretized circuits with δ=1 such that the verification results are valid in dense time. [ABSTRACT FROM AUTHOR]

We examine some extensions of the basic model, due to Alur and Dill, of real-time automata (RTA). Our model, controlled real-time automata, is a parameterized family of real-time automata with some additional features like clock stopping, variable clock velocities and periodic tests. We illustrate the power of controlled automata by presenting some languages that can be recognized deterministically by such automata, but cannot be recognized non-deterministically by any other previously introduced class of timed automata (even with ɛ-transitions). On the other hand, due to carefully chosen restrictions, controlled automata conserve basic properties of RTA: the emptiness problem is decidable and for each fixed parameter the family of recognized real-time languages is closed under boolean operations. [ABSTRACT FROM AUTHOR]

We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable. [ABSTRACT FROM AUTHOR]

Traditional methods for the analysis of system performance and reliability generally assume a precise knowledge of the system and its workload. Here, we present methods that are suited for the analysis of systems that contain partly unknown or unspecified components, such as systems in their early design stages. We introduce stochastic transition systems, a high-level formalism for the modeling of timed probabilistic systems. Stochastic transition systems extend current modeling capabilities by enabling the representation of transitions having unknown delay distributions, alongside transitions with zero or exponentially-distributed delay. We show how these various types of transitions can be uniformly represented in terms of nondeterminism, probability, fairness and time, yielding efficient algorithms for system analysis. Finally, we present methods for the specification and verification of long-run average properties of STSs. These properties include many relevant performance and reliability indices, such as system throughput, average response time, and mean time between failures. [ABSTRACT FROM AUTHOR]

We present a process algebra for the performance modeling and evaluation of concurrent systems whose activity durations are expressed through general probability distributions. We first determine the class of generalized semi-Markov processes (GSMPs) as being the class of stochastic processes on which we must rely for performance evaluation to be possible. Then we argue that in this context the right semantics for algebraic terms is a variant of the ST semantics which accounts for both functional and performance aspects. The GSMP based process algebra we propose is introduced together with its formal semantics, an example of performance evaluation, and a notion of probabilistic bisimulation based equivalence accounting for action durations which is shown to be a congruence. [ABSTRACT FROM AUTHOR]

PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example. [ABSTRACT FROM AUTHOR]

Performance evaluation is a central issue in the design of complex real-time systems. In this work, we propose an extension of so-called "Max-Plus" algebraic techniques to handle more realistic types of real-time systems. In particular, our framework encompasses graph or partial order automata, and more generally abstract models of real-time computations (including synchronous programs running over distributed architectures). To achieve this, we introduce a new dioid of partially commutative power series (transductions), whose elements encode timed behaviors. This formalism extends the traditional representation of timed event graphs by (rational) commutative transfer series with coefficients in the Max-Plus semiring. We sketch how this framework can be used to symbolically solve several problems of interest, related to real-time systems. Then we illustrate the use of this framework to encode a nontrivial mixed formalism of dataflow diagrams and automata. [ABSTRACT FROM AUTHOR]

We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output ccp semantics is preserved also when distinguishing deadlocked computations from successful ones. The systems allows to optimize CCP programs while preserving their intended meaning. Furthermore, since it preserves the deadlock behaviour of programs, it can be used for proving deadlock freeness of a class of queries in a given program. [ABSTRACT FROM AUTHOR]

We study deadlocks using geometric methods based on generalized process graphs [Dij68], i.e., cubical complexes or Higher-Dimensional Automata (HDA) [Pra91,vG91,GJ92,Gun94], describing the semantics of the concurrent system of interest. A new algorithm is described and fully assessed, both theoretically and practically and compared with more well-known traversing techniques. An implementation is available, applied to a toy language. This algorithm not only computes the deadlocking states of a concurrent system but also the so-called "unsafe region" which consists of the states which will eventually lead to a deadlocking state. Its basis is a characterization of deadlocks using dual geometric properties of the "forbidden region". [ABSTRACT FROM AUTHOR]

Reduction theorems allow one to deduce properties of a concurrent system specification from properties of a simpler, coarser-grained version called the reduced specification. We present reduction theorems based upon a more precise relation between the original and reduced specifications than earlier ones, permitting the use of reduction to reason about a larger class of properties. In particular, we present reduction theorems that handle general liveness properties. [ABSTRACT FROM AUTHOR]

We study a highly simplified version of proposals for mobility support in version 6 of Internet Protocols (IP). We concentrate on the issue of ensuring that messages to and from mobile agents are delivered without loss of connectivity. We provide three models of increasingly complex nature of a network of routers and computing agents that are interconnected via the routers. Following a detailed analysis of the three models to extract invariant properties, we show that the three models are related by a suitable notion of equivalence based on barbed bisimulation. [ABSTRACT FROM AUTHOR]

This paper introduces a compositional Hoare logics for reasoning about the correctness of systems composed of a dynamically evolving collection of processes (also called objects) which interact only via an asynchronous communication mechanism based on FIFO buffers. [ABSTRACT FROM AUTHOR]

We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of simulation preorder between pairs of processes in a class whose elements are neither finite-state nor allow finite partitioning of their state spaces. [ABSTRACT FROM AUTHOR]

During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. [ABSTRACT FROM AUTHOR]

This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR). [ABSTRACT FROM AUTHOR]

The classical theory of deterministic automata is presented in terms of the notions of homomorphism and bisimulation, which are the cornerstones of the theory of (universal) coalgebra. This leads to a transparent and uniform presentation of automata theory and yields some new insights, amongst which coinduction proof methods for language equality and language inclusion. At the same time, the present treatment of automata theory may serve as an introduction to coalgebra. [ABSTRACT FROM AUTHOR]

A non-deterministic process is viewed as a set of deterministic ones: its possible worlds. Each world represents a particular "solution" of non-determinism. Under this view of non-determinism as underspecification, nodeterministic processes are specifications, and the possible worlds represent the model space and thus the set of possible implementations. Then, refinement is inclusion of sets of possible worlds and can be used for stepwise specifications. This notion of refinement naturally induces new preorders (and equivalences) for processes that we characterize denotationally, operationally and axiomatically for a basic process algebra with nil, prefix and choice. [ABSTRACT FROM AUTHOR]

Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as "Does the implementation refine the set A of specification components without constraining the components not in A?" In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components. [ABSTRACT FROM AUTHOR]

In this paper we propose finding winning strategies of abstract games as an approach to verification problems which permits both a variable level of abstraction and on-the-fly exploration. We describe a generic algorithm which, when instantiated with certain functions specific to the concrete game, computes a winning strategy. We apply this technique to bisimulation and model-checking of value-passing processes, and to timed automata. [ABSTRACT FROM AUTHOR]

In [18, 19], we presented a theory of concurrent combinators for the asynchronous monadic π-calculus without match or summation operator [7, 16]. The system of concurrent combinators is based on a finite number of atoms and fixed interaction rules, but is as expressive as the original calculus, so that it can represent diverse interaction structures, including polyadic synchronous name passing [23] and input guarded summations [26]. The present paper shows that each of the five basic combinators introduced in [18] is indispensable to represent the whole computation, i.e. if one of the combinators is missing, we can no longer express the original calculus up to weak bisimilarity. Expressive power of several interesting subsystems of the asynchronous π-calculus is also measured by using appropriate subsets of the combinators and their variants. Finally as an application of the main result, we show there is no semantically sound encoding of the calculus into its proper subsystem under a certain condition. [ABSTRACT FROM AUTHOR]

Some applications of higher-order processes require better control of communication capabilities than what is provided by the π-calculus primitives. In particular we have found the dynamic restriction operator of CHOCS, here called blocking, useful. We investigate the consequences of adding static operators such as blocking to the first-and higher-order π-calculus. In the presence of the blocking operator (and static operators in general) the higher-order reduction of Sangiorgi, used to demonstrate the reducibility of higher-order communication features to first-order ones, breaks down. We show, as our main result, that the higher-order reduction can be regained, using an approach by which higher-order communications are replaced, roughly, by the transmission and dynamic interpretation of syntax trees. However, the reduction is very indirect, and not usable in practice. This throws new light on the position that higher-order features in the π-calculus are superfluous and not needed in practice. [ABSTRACT FROM AUTHOR]

We present complete axiomatizations of weak hypcrcongruence in the finite fragment of the fusion calculus, an extension and simplification of the π-calculus. We treat both the full fusion calculus and the subcalculus without mismatch operators. The axiomatizations are obtained from the laws for hyperequivalence and adding so called tau-laws. These are similar to the well known tau-laws for CCS and the π-calculus, but there is an interesting difference which highlights an aspect of the higher expressive power of the fusion calculus. [ABSTRACT FROM AUTHOR]

Control Flow Analysis is a static technique for predicting safe and computable approximations to the set of values that the objects of a program may assume during its execution. We present an analysis for the π-calculus that shows how names will be bound to actual channels at run time. The formulation of the analysis requires no extensions to the π-calculus, except for assigning "channels" to the occurrences of names within restrictions, and assigning "binders" to the occurrences of names within input prefixes. The result of our analysis establishes a super-set of the set of names to which a given name may be bound and of the set of names that may be sent along a given channel. Applications of our analysis include establishing simple security properties of processes. One example is that P has no leaks, i.e. P offers communication through public channels only, and confines its secret names within itself. [ABSTRACT FROM AUTHOR]

The paper presents the new computational model of Herbrand engines which combines finite-state control with uninterpreted data and function registers, thus yielding a finite representation of infinite-state machines. Herbrand engines are used to provide a high-level model of out-of-order execution in the design of micro-processors. The problem of verifying that a highly parallel design for out-of-order execution correctly implements the Instruction Set Architecture is reduced to establishing the equivalence of two Herbrand engines. We show that, for a reasonably restricted class of such engines, the equivalence problem is decidable, and present two algorithms for solving this problem. Ultimately, the appropriate statement of correctness is that the out-of-order execution produces the same final state (and all relevant intermediate actions, such as writes to memory) as a purely sequential machine running the same program. [ABSTRACT FROM AUTHOR]

PA is the process algebra allowing non-determinism, sequential and parallel compositions, and recursion. We suggest a view of PA-processes as tree languages. Our main result is that the set of (iterated) predecessors of a regular set of PA-processes is a regular tree language, and similarly for (iterated) successors. Furthermore, the corresponding tree-automata can be built effectively in polynomial-time. This has many immediate applications to verification problems for PA-processes, among which a simple and general model-checking algorithm. [ABSTRACT FROM AUTHOR]

In program synthesis, we transform a specification into a program that is guaranteed to satisfy the specification. In synthesis of reactive systems, the environment in which the program operates may behave nondeterministically, e.g., by generating different sequences of inputs in different runs of the system. To satisfy the specification, the program needs to act so that the specification holds in every computation generated by its interaction with the environment. Often, the program cannot observe all attributes of its environment. In this case, we should transform a specification into a program whose behavior depends only on the observable history of the computation. This is called synthesis with incomplete information. In such a setting, it is desirable to have a knowledge-based specification, which can refer to the uncertainty the program has about the environment's behavior. In this work we solve the problem of synthesis with incomplete information with respect to specifications in the logic of knowledge and time. We show that the problem has the same worst-case complexity as synthesis with complete information. [ABSTRACT FROM AUTHOR]

We study the problem of synthesising controllers for discrete event systems. Traditionally this problem is tackled in a linear time setting. Moreover, the desired subset of the computations of the uncontrolled system (often called a plant) is specified by automata theoretic means. Here we formulate the problem in a branching time framework. We use a class of labelled transition systems to model both the plant and the specification. We deploy behaviour preserving morphisms to capture the role of a controller; the controlled behaviour of the plant should be related via a behaviour preserving morphism to the specification at the level of unfoldings. One must go over to unfoldings in order to let the controller use memory of the past to carry out its function. We show that the problem of checking if a pair of finite transition systems — one modelling the plant and the other the specification — admits a controller is decidable in polynomial time. We also show the size of the finite controller, if one exists can be bounded by a polynomial in the sizes of the plant and the specification. Such a controller can also be effectively constructed. We then prove that in a natural concurrent setting, the problem of checking for the existence of a (finite) controller is undecidable. [ABSTRACT FROM AUTHOR]

The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model checking makes CTL a popular choice, leading to efficient model-checking tools for this logic. Can we use these tools in order to verify linear properties? In this survey paper we describe two approaches that relate branching and linear model checking. In the first approach we associate with each LTL formula ψ a CTL formula ψA that is obtained from ψ by preceding each temporal operator by the universal path quantifier A. In particular, we characterize when ψ is logically equivalent to ψA. Our second approach is motivated by the fact that the alternation-free Μ-calculus, which is more expressive than CTL, has the same computational advantage as CTL when it comes to model checking. We characterize LTL formulas that can be expressed in the alternation-free Μ-calculus; these arc precisely the formulas that are equivalent to deterministic Büchi automata. We then claim that these results are possibly of theoretical, rather than of practical interest, since in practice, LTL model checkers seem to perform rather nicely on formulas that are equivalent to CTL or alternation-free Μ-calculus formulas. [ABSTRACT FROM AUTHOR]

Recent years have seen the development of increasingly sophisticated static type systems for concurrent programming languages. Besides early detection of programming errors—the traditional domain of type systems—their applications in the concurrent setting have included strengthening behavioral equivalences and associated proof techniques, identifying confluent fragments of nonconfluent languages, and guaranteeing the absence of deadlock in certain situations. This tutorial surveys a number of type systems in the context of the picalculus [5, 6], a popular core calculus of message-based concurrency. Beginning from Milner's simple sorting discipline [6], we will touch on notions of subtyping [ABSTRACT FROM AUTHOR]