Search

A domain theoretic denotational model is given for a simple sublanguage of CCS extended with divergence operator. The model is derived as an abstraction on a suitable notion of normal forms for labelled transition systems. It is shown to be fully abstract with respect to observational precongruence.

The finitely observable, or finitary, part of bisimulation is a key tool in establishing full abstraction results for denotational semantics for process algebras with respect to bisimulation-based preorders. A bisimulation-like characterization of this relation for arbitrary transition systems is given, relying on Abramsky's characterization in terms of the finitary domain logic. More informative behavioural, observation-independent characterizations of the finitary bisimulation are also offered for several interesting classes of transition systems. These include transition systems with countable action sets, those that have bounded convergent sort and the sort-finite ones. The result for sort-finite transition systems sharpens a previous behavioural characterization of the finitary bisimulation for this class of structures given by Abramsky.AMS Subject Classification (1991): 68Q10 (Modes of computation), 68Q55(Semantics), 03B70 (Logic of Programming), 68Q90 (Transition nets).Keywords and Phrases: Concurrency, labelled transition systems with divergence,bisimulation preorder, finitary relations, domain logic for transition systems.

Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. branching congruence, eta-congruence, delay congruence and weak congruence. The completeness proofs for eta-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e. terms that may contain process variables. As a by-product, the omega-completeness of the axiomatizations is obtained as well as their completeness for closed terms. AMS Subject Classification (1991): 68Q10, 68Q40, 68Q55.CR Subject Classification (1991): D.3.1, F.1.2, F.3.2.Keywords and Phrases: Concurrency, process algebra, basic CCS, prefix iteration, branching bisimulation, eta-bisimulation, delay bisimulation, weak bisimulation, equational logic, complete axiomatizations.

A domain theoretical denotational model is given for a simple sublanguageof CCS extended with divergence operator. The model is derived asan abstraction on a suitable notion of normal forms for labelled transitionsystems. It is shown to be fully abstract with respect to observationalprecongruence.

This is the second of two companion papers on a semantic theory for communicating processes with values based on the late approach. In the first one, [Ing95], we explained the general idea of the late semantic approach. Furthermore weintroduced a general syntax for value-passing process algebra based on the late approach and a general class of denotational models for these languages in the Scott-Strachey style. Then we defined a concrete language, CCSL, which isan extension of the standard CCS with values according to the late approach.We also provided a denotational model for it, which is an instantiation of the general class. This model is a direct extension of the model given by Abramsky[Abr91] to model the pure calculus SCCS. Furthermore we gave an axiomatic semantics by means of a proof system based on inequations and proved its soundness and completeness with respect to the denotational semantics.In this paper we will give a behavioural semantics to the language CCSLin terms of a Plotkin style operational semantics and a bisimulation basedpreorder. Our main aim is to relate the behavioural view of processes we present here to the domain-theoretical one developed in the companion paper [Ing95]. In the Scott-Strachey approach an infinite process is obtained as a chain of finite and possibly partially specified processes. The completely unspecified process is given by the bottom element of the domain. An operational interpretation of this approach is to take divergence into account and give the behaviouralsemantics in terms of a prebisimulation or bisimulation preorder [Hen81,Wal90] rather than by the standard bisimulation equivalence [Par81, Mil83].One of the results in the pure case presented in [Abr91] is that the denotationalmodel given in that reference is fully abstract with respect to the "finitelyobservable" part of the bisimulation preorder but not with respect to the bisimulationpreorder which turns out to be too fine. Intuitively this is due to the algebraicity of the model and the fact that the finite elements in the modelare denotable by syntactically finite terms. The algebraicity implies that thedenotational semantics of a process is completely decided by the semantics ofits syntactically finite approximations, whereas the same can not be said about the bisimulation preorder. In fact we need experiments of an infinite depth to investigate bisimulation while this is not the case for the preorder induced by the model as explained above. An obvious consequence of this observation is that in general, a bisimulation preorder can not be expected to be modeled by an algebraic cpo given that the compact elements are denotable by syntacticallynite elements.In [Hen81] Hennessy defined a term model for SCCS. This model is !-algebraic and fails to be fully abstract with respect to the strong bisimulationpreorder. In the same paper the author introduces the notion of "the finitary part of a relation" and "a finitary relation". The finitary part of a relation R over processes, denoted by RF , is defined bypRF q i 8d:dRp) dRq where d ranges over the set of syntactically finite processes. A relation R isfinitary if RF = R. Intuitively this property may be interpreted as algebraicityat the behavioural level provided that syntactically nite terms are interpretedas compact elements in the denotational model; if a relation is nitary then itis completely decided by the syntactically nite elements.In both [Hen81] and [Abr91] the full abstractness of the respective denotationalsemantics with respect to

Fokkink ((1994) Inf. Process. Lett. 52: 333{337) has recently proposed a completeequational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),i.e., the language obtained by extending Milner's basic CCS with prefix iteration.Prefix iteration is a variation on the original binary version of the Kleene star operationp*q obtained by restricting the first argument to be an atomic action. In thispaper, we extend Fokkink's results to a setting with the unobservable action bygiving a complete equational axiomatization of Milner's observation congruence overMPA_delta^*(A_tau ). The axiomatization is obtained by extending Fokkink's axiom systemwith two of Milner's standard tau-laws and the following three equations that describethe interplay between the silent nature of tau and prefix iteration:tau . x = tau*xa*(x+tau.y) = a*(x+tau.y + a.y)tau.(a*x) = a*(tau.a*x) .Using a technique due to Groote, we also show that the resulting axiomatization isomega-complete, i.e., complete for equality of open terms.AMS Subject Classification (1991): 68Q40, 68Q42.CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.Keywords and Phrases: Minimal Process Algebra, prefix iteration, equationallogic, omega-completeness, observation congruence.

A general class of languages and denotational models for value-passingcalculi based on the late semantic approach is defined. A concrete instantiationof the general syntax is given. This is a modification of thestandard CCS according to the late approach. A denotational model forthe concrete language is given, an instantiation of the general class. Anequationally based proof system is defined and shown to be sound andcomplete with respect to the model.

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.

Late and early operational semantics are given for CCS. Late and early testing are defined and it is shown that the derived preorders coincide, contrary to what happens for bisimulation-like equivalences.

This paper introduces a process algebra which incorporates the auxiliary operators of ACP, [BK85], and is tailored towards algebraic verifications in the theory of testing equivalence. The process algebra we consider is essentially a version of ACP with the empty process in which the nondeterministic choice operators familiar from TCSP, [BHR84], and TCCS, [DH87], are used in lieu of the internal action τ and the single choice operator favoured by CCS, [Mil89], and ACP. We present a behavioural semantics for the language based upon a natural notion of testing equivalence, [DH84], and show that, contrary to what happens in a setting with the internal action τ, the left-merge operator is compatible with it. A complete equational characterization of the behavioural semantics is given for finite processes, thus providing an algebraic theory supporting the use of the auxiliary operators of ACP in algebraic verifications for testing equivalence. Finally we give a fully-abstract denotational model for finite processes with respect to the testing preorder based on a variation on Hennessy's Acceptance Trees suitable for our language.

This paper studies the equational theory of various exotic semirings presented in the literature. Exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. Two prime examples of such structures are the (max,+) semiring and the tropical semiring. It is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. For each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.

Salomaa (1969, p. 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long-standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway (1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway (1971).

Monitorability underpins the technique of runtime verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e. the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Hence, our work gives a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

Abadi and Cardelli have investigated several versions of the c-calculus, a calculus for describing central features of object-oriented programs, with particular emphasis on various type systems. In this paper we study the properties of a denotational semantics due to Abadi and Cardelli vis-a-vis the notion of observational congruence for the calculus Ob 1 . In particular, we prove that the denotational semantics based on partial equivalence relations is correct with respect to observational congruence. By means of a counter-example, we argue that the denotational model is not fully abstract with respect to observational congruence. In fact, the model is able to distinguish objects that have the same behaviour in every Ob 1 -context.

Interval temporal logics take time intervals, instead of time instants, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham's modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen's interval relations). A complete classification of all HS fragments with respect to their relative expressive power has been recently given for the classes of all linear orders and of all dense linear orders. The cases of discrete and finite linear orders turn out to be much more involved. In this paper, we make a significant step towards solving the classification problem over those classes of linear orders. First, we illustrate various non-trivial temporal properties that can be expressed by HS fragments when interpreted over finite and discrete linear orders; then, we provide a complete set of definabilities for the HS modalities corresponding to the Allen's relations meets, later, begins, finishes, and during, as well as the ones corresponding to their inverse relations. The only missing cases are those of the relations overlaps and overlapped by.

This paper presents a cancellation theorem for the preorders in van Glabbeek's linear time-branching time spectrum over BCCSP. Apart from having some intrinsic interest, the proven cancellation result plays a crucial role in the study of the cover equations, in the sense of Fokkink and Nain, that characterize the studied semantics. The techniques used in the proof of the cancellation theorem may also have some independent interest.

Concurrency as a phenomenon is observed in most of the current computer science trends. However the inherent complexity of analyzing the behavior of such a system is incremented due to the many different models of concurrency, the variety of applications and architectures, as well as the wide spectrum of specification languages and demanded correctness criteria. For the scope of this thesis we focus on state based models of concurrent computation, and on modal logics as specification languages. First we study syntactically the process algebras that describe several different concurrent behaviors, by analyzing their equational theories. Here, we use well-established techniques from the equational logic of processes to older and newer setups, and then transition to the use of more general and novel methods for the syntactical analysis of models of concurrent programs and specification languages. Our main contributions are several positive and negative axiomatizability results over various process algebraic languages and equivalences, along with some complexity results over the satisfiability of multi-agent modal logic with recursion, as a specification language., Samhliða sem fyrirbæri sést í flestum núverandi tölvunarfræði stefnur. Hins vegar er eðlislægt flókið að greina hegðun slíks kerfis- tem er aukið vegna margra mismunandi gerða samhliða, fjölbreytileikans af forritum og arkitektúr, svo og breitt svið forskrifta mælikvarða og kröfðust réttmætisviðmiða. Fyrir umfang þessarar ritgerðar leggjum við áherslu á ástandsbundin líkön af samhliða útreikningum og á formlegum rökfræði sem forskrift tungumálum. Fyrst skoðum við setningafræðilega ferlialgebrurnar sem lýsa nokkrum mismunandi samhliða hegðun, með því að greina jöfnukenningar þeirra. Hér notum við rótgróin tækni mynda jöfnunarrökfræði ferla til eldri og nýrri uppsetningar, og síðan umskipti yfir í notkun almennari og nýrra aðferða fyrir setningafræðileg greining á líkönum samhliða forrita og forskriftartungumála. Helstu framlög okkar eru nokkrar jákvæðar og neikvæðar niðurstöður um axiomatizability yfir ýmis ferli algebrumál og jafngildi, ásamt nokkrum samSveigjanleiki leiðir af því að fullnægjanleiki fjölþátta formrökfræði með endurkomu, sem a forskrift tungumál., RANNIS: `Open Problems in the Equational Logic of Processes’ (OPEL) (grant No 196050-051) Reykjavik University research fund: `Runtime and Equational Verification of Concurrent Programs' (ReVoCoP) (grant No 222021)

The ubiquitous reliance on software systems is increasing the need for ensuring their correctness. Runtime enforcement is a monitoring technique that uses moni- tors that can transform the actions of a system under scrutiny in order to alter its runtime behaviour and keep it in line with a correctness specification; these type of enforcement monitors are often called transducers. In runtime enforcement there is often no clear separation between the specification language describing the cor- rectness criteria that a system must satisfy, and the monitoring mechanism that actually ensures that these criteria are met. We thus aim to adopt a separation of concerns between the correctness specification describing what properties the sys- tem should satisfy, and the monitor describing how to enforce these properties. In this thesis we study the enforceability of the highly expressive branching time logic μHML, in a bid to identify a subset of this logic whose formulas can be adequately enforced by transducers at runtime. We conducted our study in relation to two different enforcement instrumentation settings, namely, a unidirectional setting that is simpler to understand and formalise but limited in the type of system actions it can transform at runtime, and a bidirectional one that, albeit being more complex, it allows transducers to effect and modify a wider set of system actions. During our investigation we define the behaviour of enforcement transducers and how they should be embedded with a system to achieve unidirectional and bidirectional enforcement. We also investigate what it means for a monitor to adequately enforce a logic formula, and define the necessary criteria that a monitor must satisfy in order to be adequate. Since enforcement monitors are highly intrusive, we also define a notion of optimality to use as a guide for identifying the least intrusive monitor that adequately enforces a formula. Using these enforcement definitions, we identify a μHML fragment that can be adequately enforced via enforcement transducers that drop the execution of certain actions. We then show that this fragment is maximally expressive, i.e., it is the largest subset that can be enforced via these type of enforcement monitors. We finally look into static alternatives to runtime enforcement and identify a static analysis technique that can also enforce the identified μHML fragment, but without requiring the system to execute.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.

International audience; In this short note, we establish a link between the theory of Moore Interfaces proposed in 2002 by Chakraborty et al. as a specification framework for synchronous transition systems, and the Assume/Guarantee contracts as proposed in 2007 by Benveniste et al. as a simple and flexible contract framework. As our main result we show that the operation of saturation of A/G contracts (namely the mapping (A, G) → (A, G∨¬A)), which was considered a drawback of this theory, is indeed implemented by the Moore Game of Chakraborty et al. We further develop this link and come up with some remarks on Moore Interfaces.

One of the research areas of great importance in Computer Science is the study of the semantics of concurrent reactive systems. These are systems that compute by interacting with their environment, and typically consist of several parallel components, which execute simultaneously and potentially communicate with each other. Examples of such systems range from rather simple devices such as calculators and vending machines, to programs controlling mechanical devices such as cars, subways or spaceships. In light of their widespread deployment and complexity, the application of rigorous methods for the specification, design and reasoning on the behaviour of reactive systems has always been a great challenge. One possible approach to formally handle reactive systems is to use a “common language" for describing both the actual implementations and their specifications. When following this technique, verifying whether an implementation and its specification describe the same behaviour reduces to proving some notion of equivalence/ preorder between their corresponding descriptions over the chosen language. The aim of this thesis is to exploit the strengths of a (co)algebraic framework in modelling reactive systems and reasoning on several types of associated semantics, in a uniform fashion. Moreover, we derive a suite of corresponding verification algorithms suitable for implementation in automated tools. In Chapter 3 we present a decision procedure for bisimilarity of a class of expressions defining systems such as infinite streams, deterministic automata, Mealy machines and labelled transition systems. The procedure is implemented in the automatic theorem prover CIRC. Chapter 4 provides a uniform coalgebraic handling of a series of semantics on transition systems. This is achieved by employing a generalisation of the classical powerset construction for determinising non-deterministic automata. In particular, we deal with decorated trace equivalences for labelled transition systems and probabilistic systems and, (the so-called “must” and “may”) testing semantics for divergent non-deterministic systems. The coalgebraic approach enabled reasoning on the aforementioned notions of behavioural equivalence/preorder in terms of bisimulations. Moreover, our framework facilitated the construction of verification algorithms which are not available for bisimilarity, as shown in Chapter 5. There we provide a variation of Brzozowski’s algorithm to minimise finite automata and an optimisation of Hopcroft and Karp’s algorithm for language semantics. Both algorithms were successfully applied to reason on decorated trace and testing semantics. The corresponding implementations can be tested online at: http://perso.ens-lyon.fr/damien.pous/brz/.

Structural Operational Semantics (SOS) is one of the most natural ways for providing programming languages with a formal semantics. Results on the meta-theory of SOS typically (but not solely) say that if the inference rules used in writing the semantic specification of a language conform to some syntactic template then some semantic property is guaranteed to hold or some technique is applicable in order to gain some result. These syntactic templates are called rule formats. This thesis presents four contributions on the meta-theory of SOS. As a first contribution, (1) we offer a method for establishing the validity of equations (modulo bisimilarity). The method is developed under the vest of an equivalence relation that is suitable for mechanization, the rule-matching bisimilarity. Given a semantic specification defined in SOS and given the desired equation to check, the method runs a matching, bisimulation-like, procedure in order to determine the validity of the given equation. For the method to be applicable, the SOS specification must fit a well-known rule format called GSOS, which is fairly expressive. For instance most of the process algebras can be defined within GSOS. The method is general and, not surprisingly, might not terminate. We however show that relevant equations can be checked in finite time. As another contribution, (2) we present rule formats ensuring that certain constants of a language act as zero elements. An example of zero element, though in the context of mathematics, is the number 0, that is a zero element for the multiplication operator _, i.e., x _ 0 = 0. Based on the design of one of the formats, we provide also a rule format for unit elements. The same number 0 is for instance an example of unit element for the sum operator +, as the algebraic law x + 0 = x is valid. As a third contribution, (3) we offer rule formats guaranteeing the validity of the distributivity law. Examples of distributivity laws in the context of mathematics are (x + y) _ z = (x _ z) + (y _ z), i.e., the multiplication distributes over the sum, and (A [ B) \ C = (A \ C) [ (B \ C), i.e., the set intersection distributes over the union. The algebraic laws addressed by contributions (2) and (3) are considered modulo bisimilarity. In both contributions, the proposed rule formats are mostly mechanizable and some of them are also very simple to check. Nonetheless, the rule formats we offer are expressive enough to check the validity of classic zero and unit elements as well as well-known distributivity laws from the literature. Thanks to contributions (2) and (3), now the meta-theory of SOS tackles all the basic algebraic laws, i.e., commutativity, idempotency, associativity, zero and unit elements and distributivity. Finally, (4) we propose Nominal SOS, an SOS based framework with special syntax and primitives for the definition of languages with binders. Binders bind a name in a context in order to give it a certain meaning or to denote that a special treatment for it is required. The ordinary SOS framework lacks a dedicated account for binders. Binders, however, proliferate both in mathematics (one example is the universal quantification 8x:_) and in computer science (one example is the abstraction _x:Mof the _-calculus). We provide evidence that the framework is expressive enough to model interesting calculi. For instance, we formulated the _-calculus and the _-calculus within the framework of Nominal SOS and we established the operational correctness of these formulations with regard to the original ones. We offer a suitable notion of bisimilarity that is aware of binding and we have embarked on a study of the relationship between this notion of bisimilarity and classic equivalences from the context of the _- and _-calculus. We believe that the meta-theory of SOS is by now a mature field and times are ripe for a systematic study of the meta-theory that concerns also those phenomena that are specifically related to binders. In this respect, we believe that our framework might be a good candidate to carry out such a study.