基于LTS的Statecharts操作语义研究

Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法，介绍了Statecharts及其项语法和一步语义，并基于进程代数描述Statecharts的并发行为，使用结构化的操作语义SOS规则描述Statecharts的组合语义，从而得到相应的LTS。     

Event-based operational semantics and a consistency result for real-time concurrent processes with action refinement

In this paper an event-based operational interleaving semantics is proposed for real-time processes,for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics.     

Models for name-passing processes: interleaving and causal

We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.     

On the observational theory of the CPS-calculus

We apply powerful proof-techniques of concurrency theory to study the observational theory of Thielecke’s CPS-calculus, a distillation of the target language of Continuation-Passing Style transforms. We define a labelled transition system from which we derive a (weak) labelled bisimilarity that completely characterises Morris’ context-equivalence. We prove a context lemma showing that Morris’ context-equivalence coincides with a simpler context-equivalence closed under a smaller class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris’ equivalence, in the style of Abramsky’s applicative bisimilarity. We enhance our bisimulation proof-methods with up to bisimilarity and up to context proof techniques. We use our bisimulation proof techniques to investigate a few algebraic properties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus.     

Unifying behavioral equivalences of timed transition systems

Timed transition systems are one of the most popular real-time models for concurrency. In the paper, various behavioral equivalences of timed transition systems are defined and studied. In particular, categories of this model are constructed, and their properties are studied. In addition, based on the open maps concept, abstract characterization of the considered equivalences is given. Such an approach makes it possible to develop a metatheory designed for unified definition and study of timed behavioral equivalences in the “linear time-branching time” spectrum of semantics.     

A uniform approach to three-valued semantics for <Emphasis Type="Italic">μ</Emphasis>-calculus on abstractions of hybrid automata

In this paper, we consider the definition of a three-valued semantics for a μ-calculus on abstractions of hybrid automata. To this end, we first develop a framework that is general in the sense that it provides a preservation result for several possible semantics of the modal operators. In a second step, we instantiate our framework to two particular abstractions. To this end, a key issue is the consideration of both over- and underapproximated reachability, while classic simulation-based abstractions rely only on overapproximations, and therefore limit the preservation to the universal (μ-calculus’) fragment. To specialize our general result, we consider (1) modal abstractions, where the notions of ‘may’ and ‘must’ transitions are extended from the purely discrete to the hybrid time framework, and (2) so-called discrete bounded bisimulation abstractions.     

Institution Morphisms

Institutions formalise the intuitive notion of logical system, including syntax, semantics, and the relation of satisfaction between them. Our exposition emphasises the natural way that institutions can support deduction on sentences, and inclusions of signatures, theories, etc.; it also introduces terminology to clearly distinguish several levels of generality of the institution concept. A surprising number of different notions of morphism have been suggested for forming categories with institutions as objects, and an amazing variety of names have been proposed for them. One goal of this paper is to suggest a terminology that is uniform and informative to replace the current chaotic nomenclature; another goal is to investigate the properties and interrelations of these notions in a systematic way. Following brief expositions of indexed categories, diagram categories, twisted relations and Kan extensions, we demonstrate and then exploit the duality between institution morphisms in the original sense of Goguen and Burstall, and the ‘plain maps’ of Meseguer, obtaining simple uniform proofs of completeness and cocompleteness for both resulting categories. Because of this duality, we prefer the name ‘comorphism’ over ‘plain map’; moreover, we argue that morphisms are more natural than comorphisms in many cases. We also consider ‘theoroidal’ morphisms and comorphisms, which generalise signatures to theories, based on a theoroidal institution construction, finding that the ‘maps’ of Meseguer are theoroidal comorphisms, while theoroidal morphisms are a new concept. We introduce ‘forward’ and ‘semi-natural’ morphisms, and develop some of their properties. Appendices discuss institutions for partial algebra, a variant of order sorted algebra, two versions of hidden algebra, and a generalisation of universal algebra; these illustrate various points in the main text. A final appendix makes explicit a greater generality for the institution concept, clarifies certain details and proves some results that lift institution theory to this level. Received December 2000 / Accepted in revised form January 2002     

Probabilistic bisimulations for quantum processes

Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model named qCCS. It is a natural quantum extension of classical value-passing CCS which can deal with input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given in terms of probabilistic labeled transition system. This semantics has many different features compared with the proposals in the available literature in order to describe the input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, the notions of strong probabilistic bisimulation and weak probabilistic bisimulation between quantum processes are introduced. Furthermore, some properties of these two probabilistic bisimulations, such as congruence under various combinators, are examined.     

Time-Abstracted Bisimulation: Implicit Specifications and Decidability

In the last few years a number of real-time process calculi have emerged with the purpose of capturing important quantitative aspects of real-time systems. In addition, a number of process equivalences sensitive to time-quantities have been proposed, among these the notion of timed (bisimulation) equivalence. In this paper, we introduce atime-abstracting(bisimulation) equivalence and investigate its properties with respect to the real-time process calculus of Wang (Real-time behaviour of asynchronous agents,in“Proceedings of CONCUR90,” Lecture Notes in Computer Science, Vol. 458, Springer-Verlag, Berlin/New York, 1990). Seemingly, such an equivalence would yield very little information (if any) about the timing properties of a process. However, time-abstracted reasoning about a composite process may yield important information about the relative timing-properties of the components of the system. In fact, we show as a main theorem that such implicit reasoning will revealalltiming aspects of a process. More precisely, we prove that two processes are interchangeable in any context up to time-abstracted equivalence precisely if the two processes are themselves timed equivalent. As our second main theorem, we prove that time-abstracted equivalence is decidable for the calculus of Wang, using classical methods based on a finite-state symbolic, structured operational semantics.     

A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions

This paper discusses a timed variant of a process algebra akin to LOTOS, baptized UPA, in a causality-based setting. Two timed features are incorporated—a delay function which constrains the occurrence time of atomic actions and an urgency operator that forces (local or synchronized) actions to happen urgently. Timeouts are typical urgent phenomena. A novel timed extension of event structures is introduced and used as a vehicle to provide a denotational causality-based semantics for UPA. Recursion is dealt with by using standard fixpoint theory. In addition, an operational semantics is presented based on separate time- and action-transitions that is shown to be consistent with the event structure semantics. An interleaving semantics for UPA is immediately obtained from the operational semantics. By adopting this dual approach the well-developed timed interleaving view is extended with a consistent timed partial order view and a comparison is facilitated of the partial order model and the variety of existing (interleaved) timed process algebras.     

Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in π-calculus.However,it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly.In this paper a new notion of bisimulation is introduced,in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names.It is shown that the new notion captures symbolic bisimulation in a precise sense.Based on the new definition an efficient algorithm,which instantiates input names “on-the -fly“,is presented to check bisimulations for finite-control π-calculus.     

Enhanced event structures: Towards a true concurrency semantics for E-LOTOS

E-LOTOS is a standard process-algebraic language for formal specification of real-time concurrent and reactive systems. Its originally defined semantics is based on interleaving of events. In the present paper, we propose an enhanced kind of event structures and show how to employ them to give E-LOTOS processes a branching-time true concurrency semantics. The proposed event structures can model real-time processes with data handling and excel in concise representation of event renaming and synchronization.     

Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) [51] and [53]), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects.The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics.That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.     

Process algebra with guards: Combining Hoare logic with process algebra

We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs such as if — then — else — fi and while — do — od.The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data-)state. The data-states are given by a data environment that also defines in which data-states guards hold and how atomic actions (non-deterministically) transform these states. The operational semantics is studied modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) we present a small axiom system that is complete with respect to a general class of data environments. Given a particular data environmentL we add three axioms to this system, which is then again complete, provided weakest preconditions are expressible andL is sufficiently deterministic.Then we study process algebra with parallelism and guards. A two phase-calculus is provided that makes it possible to prove identities between parallel processes. Also this calculus is complete. In the last section we show that partial correctness formulas can easily be expressed in this setting. We use process algebra with guards to prove the soundness of a Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.Supported by ESPRIT Basic Research Action no. 3006 (CONCUR) and by RACE project no. 1046 (SPECS).Supported by RACE project no. 1046 (SPECS).     

Refinement of Actions in a Real-Time Process Algebra with a True Concurrency Model

In this paper, we develop techniques of action refinement in a real-time process algebra that allows urgent interactions to model timeout. Semantic counterpart is carried out in a real-time non-interleaving causality based setting, timed bundle event structures. We show that our refinement notions have the following nice properties: the observable behaviour of the refined system can be inferred compositionally from the observable behaviour of the original system and from the observable behaviour of the processes substituted for the actions; the timed extensions of observational pomset trace equivalence and observational history preserving bisimulation equivalence are both congruences under our refinement; and the syntactic and semantic refinements coincide up to the aforementioned equivalence relations with respect to a cpo-based denotational semantics.     

Deciding orthogonal bisimulation

Bergstra, Ponse and van der Zwaag introduced in 2003 the notion of orthogonal bisimulation equivalence on labeled transition systems. This equivalence is a refinement of branching bisimulation, in which consecutive tau’s (silent steps) can be compressed into one (but not zero) tau’s. The main advantage of orthogonal bisimulation is that it combines well with priorities. Here we solve the problem of deciding orthogonal bisimulation equivalence in finite (regular) labeled transition systems. Unlike as in branching bisimulation, in orthogonal bisimulation, cycles of silent steps cannot be eliminated. Hence, the algorithm of Groote and Vaandrager (1990) cannot be adapted easily. However, we show that it is still possible to decide orthogonal bisimulation with the same complexity as that of Groote and Vaandrager’s algorithm. Thus if n is the number of states, and m the number of transitions then it takes O(n(m + n)) time to decide orthogonal bisimilarity on finite labeled transition systems, using O(m + n) space. J. Parrow     

The theory of interactive generalized semi-Markov processes

In this paper we introduce the calculus of interactive generalized semi-Markov processes (IGSMPs), a stochastic process algebra which can express probabilistic timed delays with general distributions and synchronizable actions with zero duration, and where choices may be probabilistic, non-deterministic and prioritized. IGSMP is equipped with a structural operational semantics which generates semantic models in the form of generalized semi-Markov processes (GSMPs), i.e. probabilistic systems with generally distributed time, extended with action transitions representing interaction among system components. This is obtained by expressing the concurrent execution of delays through a variant of ST semantics which is based on dynamic names. The fact that names for delays are generated dynamically by the semantics makes it possible to define a notion of observational congruence for IGSMP (that abstracts from internal actions with zero duration) simply as a combination of standard observational congruence and probabilistic bisimulation. We also present a complete axiomatization for observational congruence over IGSMP. Finally, we show how to derive a GSMP from a given IGSMP specification in order to evaluate the system performance and we present a case study.     

Towards action refinement for true concurrent real time

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper we develop a theory of action refinement in a real-time non-interleaving causality based setting, a timed extension of bundle event structures that allows for urgent interactions to model timeout. The syntactic action refinement operation is presented in a timed process algebra as incorporated in the internationally standardised specification language LOTOS. We show that the behaviour of the refined system can be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions with explicitly represented start points, that the timed versions of a linear-time equivalence, termed pomset trace equivalence, and a branching-time equivalence, termed history preserving bisimulation equivalence, are both congruences under the refinement, and that the syntactic and semantic action refinements developed coincide under these equivalence relations with respect to a metric denotational semantics. Therefore, our refinement operations behave well. They meet the commonly expected properties.Received: 9 January 2003     

Scope control and grammatical dependencies

This paper develops a semantics with control over scope relations using Vermeulen’s stack valued assignments as information states. This makes available a limited form of scope reuse and name switching. The goal is to have a general system that fixes available scoping effects to those that are characteristic of natural language. The resulting system is called Scope Control Theory, since it provides a theory about what scope has to be like in natural language. The theory is shown to replicate a wide range of grammatical dependencies, including options for, and constraints on, ‘donkey’, ‘binding’, ‘movement’, ‘Control’ and ‘scope marking’ dependencies.