Search

To specify and verify the concurrent and reactive systems with the theorem proving approach, a complete axiomatization is formalized for first order projection temporal logic (PTL) with both finite and infinite time. To this end, PTL is restricted to a finite domain, and the syntax, semantics as well as the axiomatization of PTL are presented. Further, the techniques of labeled normal form and labeled normal form graph of PTL formulas are introduced respectively, with which a decision procedure for quantifier free PTL (QFPTL) formulas is given. Moreover, a generalized labeled normal form graph is defined and employed to transform a quantified PTL formula into its equivalent QFPTL formula. Finally, a decision procedure for PTL is formalized and the completeness of the axiomatic system is proved based on the decidability of PTL formulas.

In this paper we develop an axiomatic approach to structured specifications in which both the underlying logical system and corresponding institution of the structured specifications are treated as abstract institutions, which means two levels of institution independence. This abstract axiomatic approach provides a uniform framework for the study of structured specifications independently from any actual choice of specification building operators, and moreover it unifies the theory and the model oriented approaches. Within this framework we develop concepts and results about ‘abstract structured specifications’ such as co-limits, model amalgamation, compactness, interpolation, sound and complete proof theory, and pushout-style parameterization with sharing, all of them in a top down manner dictated by the upper level of institution independence.

In this work, we address some issues related to products of graphs and products of modal logics. Our main contribution is the presentation of a necessary and sufficient condition for a countable and connected graph to be a product, using a property called intransitivity. We then proceed to describe this property in a logical language. First, we show that intransitivity is not modally definable and also that no necessary and sufficient condition for a graph to be a product can be modally definable. Then, we exhibit a formula in a hybrid language that describes intransitivity. With this, we get a logical characterization of products of graphs of arbitrary dimensions. We then use this characterization to obtain two other interesting results. First, we determine that it is possible to test in polynomial time, using a model-checking algorithm, whether a finite connected graph is a product. This test has cubic complexity in the size of the graph and quadratic complexity in its number of dimensions. Finally, we use this characterization of countable connected products to provide sound and complete axiomatic systems for a large class of products of modal logics. This class contains the logics defined by product frames obtained from Kripke frames that satisfy connectivity, transitivity and symmetry plus any additional property that can be defined by a pure hybrid formula. Most sound and complete axiomatic systems presented in the literature are for products of a pair of modal logics, while we are able, using hybrid logics, to provide sound and complete axiomatizations for many products of arbitrary dimensions.

We present some rst-order probability logics. The logics allow making statements such as P>s, with the intended meaning \the probability of truthfulness of is greater than or equal to s". We describe the corresponding probability models. We give a sound and complete innitary axiomatic system for the most general of our logics, while for some restrictions of this logic we provide nitary axiomatic systems. We study the decidability of our logics. We discuss some of the related papers. c 2000 Elsevier Science B.V. All rights reserved.

Statecharts is a behavioural specification language proposed for specifying large real-time, event-driven reactive systems. It is a graphical language based on state-transition diagrams for finite state machines extended with many features like hierarchy, concurrency, broadcast communication and time-out. We supply Statecharts with a compositional axiomatization for both safety and liveness properties. By generating external events symbolically, Statecharts can be executed, thereby turning it into a programming language for real-time concurrency (as well as enabling rapid prototyping). As such it is well suited for compositional program verification. In addition to our compositional axiomatic system, we give a denotational semantics and prove that the axiomatization is sound and relatively complete with respect to this semantics.

The paper proposes an axiomatic approach to specification languages, and introduces notions of reducibility and equivalence as tools for their study and comparison. Algebraic specification languages are characterized up to equivalence. They are shown to be limited in expressive power by implicational languages.

Two ways of describing the behaviour of concurrent systems have widely been suggested: arbitrary interleaving and partial orders. Sometimes the latter has been claimed superior because concurrency is represented in a ‘true’ way; on the other hand, some authors have claimed that the former is sufficient for all practical purposes. Petri net theory offers a framework in which both kinds of semantics can be defined formally and hence compared with each other. Occurence sequences correspond to interleaved behaviour while the notion of a process is used to capture partial-order semantics. This paper aims at obtaining formal results about the relationship between various classes of processes and occurence sequences in net theory. We shall compare an axiomatic approach to the definition of processes with an inductive approach which relates processes to occurence sequences (and generalisations thereof). We shall show that, in general, axiomatic process semantics is more powerful than inductive semantics using occurence sequences. However, we shall also show that the latter can be generalised, or the former be restricted, to yield various equivalence results. The structure of the relation between sequences and processes will also be explored, exhibiting two meaningful relations, one on the sequences and one on the processes, which correspond to each other bijectively. We shall apply and simplify the theory to the practically important case of nets which are of finite synchronisation and 1-safe.

An axiomatic theory of sets and rules is formulated, which permits the use of sets as data structures and allows rules to operate on rules, numbers, or sets. We might call it a “polymorphic set theory”. Our theory combines the λ-calculus with traditional set theories. A natural set-theoretic model of the theory is constructed, establishing the consistency of the theory and bounding its proof-theoretic strength, and giving in a sense its denotational semantics. Another model, a natural recursion-theoretic model, is constructed, in which only recursive operations from integers to integers are represented, even though the logic can be classical. Some related philosophical considerations on the notions of set, type, and data structure are given in an appendix.

In this paper we propose an axiomatic semantics for the synchronous language Esterel. We begin with giving a structural operational semantics for Esterel in terms of a labeled transition system (LTS). We prove that bisimulation on LTS states (which correspond to Esterel programs) is a congruence and that our LTS reflects the input/output behavior of programs. So, bisimilar programs are distinguished neither by any Esterel context nor by the external environment, and bisimulation is a reasonable notion of behavioral equivalence. In order to characterize equivalent programs, we give a set of axioms and we prove that they induce an axiomatization over Esterel which is sound and complete modulo bisimulation.

The paper investigates the nonsymbolic algebraic semantics of the weak bisimulation congruences on finite pi processes. The weak bisimulation congruences are studied both in the absence and in the presence of the mismatch operator. Some interesting phenomena about the open congruences are revealed. Several new tau laws are discovered and their relationship is discussed. The contributions of the paper are mainly as follows: 1.It is proved that Milner's three tau laws fail to lift a complete system for the strong open congruence to a complete system for the weak open congruence in the absence of both the mismatch operator and the restriction operator. A fourth tau law is proposed to deal with the match operator under the prefix operation. It is shown that for this calculus a complete system for the strong open congruence extended with all the four tau laws is complete for the weak open congruence.2.It is verified that the four tau laws are also enough for the weak open congruence of the pi calculus without the mismatch operator. A complete system using distinctions is given.3.It is pointed out that the standard definition of the weak open congruence gives rise to a bad equivalence relation in the presence of the mismatch operator. Two alternatives are proposed. These are the late open congruence and the early open congruence. Their difference is similar to that between the weak late congruence and the weak early congruence. Complete axiomatic systems for the two weak open congruences are given.

Data flow networks are a model of concurrent computation. They consist of a collection of concurrent asynchronous processes which communicate by sending data over FIFO channels. In this paper we study the algebraic structure of the data flow networks and base their semantics on stream processing functions. Our algebraic theory is based on the calculus of flownomials. With an additive (or cantorian) interpretation the calculus gives a unified presentation of the classical algebraic models for control structures, that is, regular algebra and iteration theories. The kernel of the calculus is an equational axiomatization called basic network algebra (BNA) for flow graphs modulo graph isomorphism. We show that the algebra of stream processing functions called SPF (used for deterministic networks) and the algebra of sets of stream processing functions called P SPF (used for nondeterministic networks) are BNA algebras. Actually they give a multiplicative (or cartesian) interpretation of the calculus of flownomials. As a byproduct this shows that both semantic models are compositional. This means the semantics of a network may be described in terms of the semantics of its components. (As it is well known this is not true for the input–output relational semantics of nondeterministic networks.) We also identify additional axioms satisfied by the branching constants in these two algebraic theories. For the deterministic case we study in addition the coarser equivalence relation on networks given by the input–output behavior and provide a correct and complete axiomatization.

A semantic algebra construction is introduced to model the stepwise behavior of synchronous systems in an arbitrary pointed algebraic theory T . The theory T is extended to a feedback theory F ∞ T in which the bottom morphism is the designated point of T . The feedback theory F ∞ T is obtained as the inverse limit of the theories n -res T that describe the stepwise behavior of systems in T restricted to the first n clock cycles. It is shown that in F ∞ T , iteration satisfies the functorial dagger condition. Some suggestions are made about how to generalize the construction to handle infinite systems.

We give a finite equational axiomatization for +-free identities of (regular) languages which contain the empty word. The axioms for the whole equational theory of such languages were given by Yanov.