Search

In this paper we present various notions of the combined refinement for data and processes within the specification language Csp-Casl. We develop proof support for our refinement notions and demonstrate how to employ them for system development and for system analysis. Finally, we apply our technique to an industrial standard for an electronic payment system. [ABSTRACT FROM AUTHOR]

We introduce two institutions for the process algebra Csp, one for the traces model, and one for the stable failures model. The construction is generic and should be easily instantiated with further models. As a consequence, we can use structured specification constructs like renaming, hiding and parameterisation (that have been introduced over an arbitrary institution) also for Csp. With a small example we demonstrate that structuring indeed makes sense for Csp. [ABSTRACT FROM AUTHOR]

Traditionally, the various semantics of the process algebra Csp are formulated in denotational style. For many Csp models, e.g., the traces model, equivalent semantics have been given in operational style. A Csp semantics in axiomatic style, however, has been considered problematic in the literature. In this paper we present a sound and complete axiomatic semantics for Csp with unbounded nondeterminism over an alphabet of arbitrary size. This result is connected in various ways with our tool Csp-Prover: (1) the Csp dialect under discussion is the input language of Csp-Prover; (2) all theorems presented have been verified with Csp-Prover; (3) Csp-Prover implements the given axiom system. [ABSTRACT FROM AUTHOR]

In the traditional formal approach to system specification and implementation, the software development process consists of a number of refinement steps which transform the initial specification into its correct realisation. This idealised view can hardly capture common situations when a specification changes in a non-incremental way. An extra flexibility can be added to the development process by allowing for a redesign of specifications, in addition to refinement steps. In this paper, the notion of specification redesign is formalised for an arbitrary institution. Basic properties of redesign are investigated and the formalism is applied to provide a formal semantics for UML class diagram transformations. As examples, two refactoring patterns are described in terms of class diagrams and interpreted as redesigns of corresponding algebraic specifications. [ABSTRACT FROM AUTHOR]

Following the paradigm of encapsulation of side effects via monads, the Java execution mechanism has been described by the so-called Java monad, encorporating essentially stateful computation and exceptions, which are heavily used in Java control flow. A technical problem that appears in this model is the fact that the return exception in Java is parametrized by the return value, so that method calls actually move between slightly different monads, depending on the type of the return value. We provide a treatment of this problem in the general framework of exception monads as introduced in earlier work by some of the authors; this framework includes generic partial and total Hoare calculi for abrupt termination. Moreover, we illustrate this framework by means of a verification of a pattern match algorithm. [ABSTRACT FROM AUTHOR]

Multialgebras generalise algebraic semantics to handle nondeterminism. They model relational structures, representing relations as multivalued functions by selecting one argument as the "result". This leads to strong algebraic properties missing in the case of relational structures. However, such strong properties can be obtained only by first choosing appropriate notion of homomorphism. We summarize earlier results on the possible notions of compositional homomorphisms of multialgebras and investigate in detail one of them, the outer-tight homomorphisms which yield rich structural properties not offered by other alternatives. The outer-tight homomorphisms are different from those obtained when relations are modeled as coalgebras and the associated congruence is the converse bisimulation equivalence. The category is cocomplete but initial objects are of little interest (essentially empty). On the other hand, the category does not, in general, possess final objects for the usual cardinality reasons. The main objective of the paper is to show that Aczel's construction of final coalgebras for set-based functors can be modified and applied to multialgebras. We therefore extend the category admitting also structures over proper classes and show the existence of final objects in this category. [ABSTRACT FROM AUTHOR]

A measure polynomial functor is a functor in the category built up from constant measurable spaces, the identity functor and using products, coproducts and the probability measure functor Δ. In [1] it was proved that these functors have final coalgebras. We present here a different proof of that fact, one that uses the final sequence of the functor, instead of an ad hoc language. We also show how this method works for certain functors in and explore the connection with results in the literature that use the final sequence in other ways. [ABSTRACT FROM AUTHOR]

We propose a method called back-and-forth narrowing for solving reachability goals of the form in general term rewrite systems. The method is a complete semi-decision procedure in the sense that it is guaranteed to find a solution when one exists, but in general it may not terminate when there are no solutions. The completeness result is very general in that it makes no assumptions about the given term rewrite system. Specifically, the rewrite rules need not be linear, confluent, or terminating, and can even have extra-variables in the righthand side. Such generality is often essential while modeling concurrent systems or axiomatizing inference systems as rewrite rules, and in such applications back-and-forth narrowing can be used as a sound and complete technique for symbolic reachability analysis or as a deductive procedure for proving existential formulae. [ABSTRACT FROM AUTHOR]

Event-pattern reactive programs are front-end programs for distributed reactive components that preprocess an incoming stream of event stimuli. Their purpose is to recognize temporal patterns of events that are relevant to the serviced program and ignore all other events, outsourcing some of the component's complexity and shielding it from event overload. Correctness of event-pattern reactive programs is essential, because bugs may result in loss of relevant events and hence failure to react appropriately. We introduce PAR, a specification language for event-pattern reactive programs. We propose a new approach for defining such languages in terms of observations and actions. This approach applies standard techniques from coalgebra to obtain instances of the corecursion and coinduction principles. Corecursion is used to formally de.ne the operational semantics of PAR, and coinduction allows to prove general equivalences between (ground and parameterized) PAR programs. This is the first of a series of papers in which we study questions of expressive completeness, complexity, and formal verification techniques for specification languages of event-pattern reactive programs. [ABSTRACT FROM AUTHOR]

We introduce the notion of discrete countable Lawvere V-theory and study constructions that may be made on it. The notion of discrete countable Lawvere V-theory extends that of ordinary countable Lawvere theory by allowing the homsets of an ordinary countable Lawvere theory to become homobjects of a well-behaved axiomatically defined category such as that of ω-cpo's. Every discrete countable Lawvere V-theory induces a V-enriched monad, equivalently a strong monad, on V. We show that discrete countable Lawvere V-theories allow us to model all the leading examples of computational effects other than continuations, and that they are closed under constructions of sum, tensor and distributive tensor, which are the fundamental ways in which one combines such effects. We also show that discrete countable Lawvere V-theories are closed under taking an image, allowing one to treat observation as a mathematical primitive in modelling effects. [ABSTRACT FROM AUTHOR]

We show that any institution satisfying some reasonable conditions can be transformed into another institution, , which captures formally and abstractly the intuitions of adding support for behavioral equivalence and reasoning to an existing, particular algebraic framework. We call our transformation an "extension" because has the same sentences as and because its entailment relation includes that of . Many properties of behavioral equivalence in concrete hidden logics follow as special cases of corresponding institutional results. As expected, the presented constructions and results can be instantiated to other logics satisfying our requirements as well, thus leading to novel behavioral logics, such as partial or infinitary ones, that have the desired properties. [ABSTRACT FROM AUTHOR]

Simulations are a very natural way of relating concurrent systems, which are mathematically modeled by Kripke structures. The range of available notions of simulations makes it very natural to adopt a categorical viewpoint in which Kripke structures become the objects of several categories while the morphisms are obtained from the corresponding notion of simulation. Here we define in detail several of those categories, collect them together in various institutions, and study their most interesting properties. [ABSTRACT FROM AUTHOR]

This paper provides a general account of the notion of recursive program schemes, their uninterpreted and interpreted solutions, and related concepts. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with "enough final coalgebras" we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study recursion, e. g., substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes at all. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme. In this short version of our paper we can only sketch some proofs. [ABSTRACT FROM AUTHOR]

In this paper we present FLRS, a sound and complete equational logic for proving the equivalence of recursive program schemes. We use extended versions of the Solution Theorems from [1] and [2] to provide coalgebraic semantics to recursive program schemes. We end the paper with a proof that FLRS is complete with respect to the coalgebraic semantics. [ABSTRACT FROM AUTHOR]

This paper studies finitary modal logics as specification languages for Set-coalgebras (coalgebras on the category of sets) using Stone duality. It is well-known that Set-coalgebras are not semantically adequate for finitary modal logics in the sense that bisimilarity does not in general coincide with logical equivalence. Stone-coalgebras (coalgebras over the category of Stone spaces), on the other hand, do provide an adequate semantics for finitary modal logics. This leads us to study the relationship of finitary modal logics and Set-coalgebras by uncovering the relationship between Set-coalgebras and Stone-coalgebras. This builds on a long tradition in modal logic, where one studies canonical extensions of modal algebras and ultrafilter extensions of Kripke frames to account for finitary logics. Our main contributions are the generalisations of two classical theorems in modal logic to coalgebras, namely the Jónsson-Tarski theorem giving a set-theoretic representation for each modal algebra and the bisimulation-somewhere-else theorem stating that two states of a coalgebra have the same (finitary modal) theory iff they are bisimilar (or behaviourally equivalent) in the ultrafilter extension of the coalgebra. [ABSTRACT FROM AUTHOR]

Every endofunctor B on the category can be lifted to a fibred functor on the category (fibred over ) of equivalence relations and relation-preserving functions. In this paper, the least (fibre-wise) of such liftings, L(B), is characterized for essentially any B. The lifting has all the useful properties of the relation lifting due to Jacobs, without the usual assumption of weak pullback preservation; if B preserves weak pullbacks, the two liftings coincide. Equivalence relations can be viewed as Boolean algebras of subsets (predicates, tests). This correspondence relates L(B) to the least test suite lifting T(B), which is defined in the spirit of predicate lifting as used in coalgebraic modal logic. Properties of T(B) translate to a general expressivity result for a modal logic for B-coalgebras. In the resulting logic, modal operators of any arity can appear. [ABSTRACT FROM AUTHOR]

Recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. Due to the complexity of the involved spatial reduction, there is — in contrast to the situation in standard process algebra — up to now no satisfying coalgebraic representation of a mobile process calculus. Here, we discuss work towards a unifying coalgebraic framework for the denotational semantics of mobile systems. The connection between the ambient calculus and a coalgebraic approach which uses an extension of labelled transition systems in the representation of the reduction relation is analyzed in more detail. The formal representation of this framework is cast in the algebraic-coalgebraic specification language CoCasl. [ABSTRACT FROM AUTHOR]

We show that, for functors with suitable mild restrictions, the initial algebra in the category of sets and functions gives rise to the final coalgebra in the (Kleisli) category of sets and relations. The finality principle thus obtained leads to the finite trace semantics of non-deterministic systems, which extends the trace semantics for coalgebras previously introduced by the second author. We demonstrate the use of our technical result by giving the first coalgebraic account on context-free grammars, where we obtain generated context-free languages via the finite trace semantics. Additionally, the constructions of both finite and possibly infinite parse trees are shown to be monads. Hence our extension of the application domain of coalgebras identifies several new mathematical constructions and structures. [ABSTRACT FROM AUTHOR]

For any set-endofunctor there exists a largest sub-cartesian transformation μ to the filter functor . Thus we can associate with every T-coalgebra A a certain filter-coalgebra . Precisely, when T (weakly) preserves preimages, μ is natural, and when T (weakly) preserves intersections, μ factors through the covariant powerset functor , thus providing for every T-coalgebra A a Kripke structure . We characterize preservation of preimages, preservation of intersections, and preservation of both preimages and intersections via the existence of natural, sub-cartesian or cartesian transformations from T to either or . Moreover, we define for arbitrary T-coalgebras a next-time operator with associated modal operators and and relate their properties to weak limit preservation properties of T. In particular, for any T-coalgebra there is a transition system with if and only if T preserves intersections. [ABSTRACT FROM AUTHOR]

In the specific situation of formal reasoning concerned with "regular expression equivalence" we address instances of more general questions such as: how can coinductive argumentation be formalised logically and be applied effectively, as well as how is it linked to traditional forms of proof. For statements expressing that two regular expressions are language equivalent, we demonstrate that proofs by coinduction can be formulated in a proof system based on equational logic, where effective proof-search is possible. And we describe a proof-theoretic method for translating derivations in this proof system into a "traditional" axiom system: namely, into a "reverse form" of the axiomatisation of "regular expression equivalence" due to Salomaa. Hereby we obtain a coinductive completeness proof for the traditional proof system. [ABSTRACT FROM AUTHOR]

The proof system has been used to implement an algebraic framework for verifying the correctness of hardware with input and output. Implementations and specifications are modelled as iterated maps, with input and output modelled using streams. The correctness model supports three types of abstraction: temporal abstraction (with immersions), data abstraction, and stream abstraction. This work has been used to formally verify the 6 microprocessor. This paper discusses this processor's input and output behaviour and shows how this has been modelled and verified in . The verification is believed to be the first complete formal verification of a commercial off-the-shelf (COTS) processor. The definition of correctness given here is new - it is suited to verifying block data transfer instructions, these load and store sets of registers. [ABSTRACT FROM AUTHOR]

We propose a coalgebraic model of the Fusion calculus based on HD-automata. The main advantage of the approach is that the partition refinement algorithm designed for HD-automata is easily adapted to handle Fusion calculus processes. Hence, the transition systems of Fusion calculus processes can be minimised according to the notion of observational semantics of the calculus. As a beneficial side effect, this also provides a bisimulation checker for Fusion calculus. [ABSTRACT FROM AUTHOR]

Simple systems cannot decomposed further. Algebraically, simple systems have only isomorphisms as epis. We characterize simple stochastic relations through different forms of bisimulations for the case that the underlying spaces are Polish, and analytic, respectively. This requires a closer investigation of bisimulations, congruences and their mutual relationship. We provide a complete characterization of simple stochastic relations for analytic spaces. [ABSTRACT FROM AUTHOR]

There are several approaches to the problem of giving a categorical semantics to Martin-Löf type theory with dependent sums and products and extensional equality types. The most established one relies on the notion of a type-category (or category with attributes) with Σ and Π types. We extend such a semantics by introducing coinductive types both on the syntactic level and in a type-category. Soundness of the semantics is preserved. As an example of such a category, we prove that the type-category built over a locally cartesian closed category admits coinductive types whenever has final coalgebras for all polynomial functors. [ABSTRACT FROM AUTHOR]

The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature, at different levels of abstraction. We focus on a basic algebra of connectors which is expressive enough to model, e.g., all the architectural connectors of CommUnity. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization. [ABSTRACT FROM AUTHOR]

We present ACPc, a process algebra with conditional expressions in which the conditions are taken from a Boolean algebra, and extensions of this process algebra with mechanisms for condition evaluation. We confine ourselves to finitely branching processes. This restriction makes it possible to presentc in a concise and intuitively clear way, and to bring the notion of splitting bisimulation equivalence and the issue of condition evaluation in process algebras with conditional expressions to the forefront. [ABSTRACT FROM AUTHOR]

The intersection of algebra and coalgebra, i.e., the collection of all categories that are varieties as well as covarieties, is proved to consist of precisely the presheaf categories. [ABSTRACT FROM AUTHOR]

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's Basic Process Algebra with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based. [ABSTRACT FROM AUTHOR]

We consider open terms and parametric rules in the context of the systematic derivation of labelled transitions from reduction systems. [ABSTRACT FROM AUTHOR]

We study structures which have arisen in recent work by the present author and Bob Coecke on a categorical axiomatics for Quantum Mechanics; in particular, the notion of strongly compact closed category. We explain how these structures support a notion of scalar which allows quantitative aspects of physical theory to be expressed, and how the notion of strong compact closure emerges as a significant refinement of the more classical notion of compact closed category. We then proceed to an extended discussion of free constructions for a sequence of progressively more complex kinds of structured category, culminating in the strongly compact closed case. The simple geometric and combinatorial ideas underlying these constructions are emphasized. We also discuss variations where a prescribed monoid of scalars can be ‘glued in' to the free construction. [ABSTRACT FROM AUTHOR]

We describe a new tool called Csp-Prover which is an interactive theorem prover dedicated to refinement proofs within the process algebra Csp. It aims specifically at proofs for infinite state systems, which may also involve infinite non-determinism. Semantically, Csp-Prover supports both the theory of complete metric spaces as well as the theory of complete partial orders. Both these theories are implemented for infinite product spaces. Technically, Csp-Prover is based on the theorem prover Isabelle. It provides a deep encoding of Csp. The tool's architecture follows a generic approach which makes it easy to adapt it for various Csp models besides those studied here: the stable failures model and the traces model . [ABSTRACT FROM AUTHOR]

We introduce the Casl Consistency Checker (CCC), a tool that supports consistency proofs in the algebraic specification language Casl. CCC is a faithful implementation of a previously described consistency calculus. Its system architecture combines flexibility with correctness ensured by encapsulation in a type system. CCC offers tactics, tactical combinators, forward and backward proof, and a number of specialised static checkers, as well as a connection to the Casl proof tool HOL-Casl to discharge proof obligations. We demonstrate the viability of CCC by an extended example taken from the Casl standard library of basic datatypes. [ABSTRACT FROM AUTHOR]

This paper describes the formal specification of a future banking system by abstract data types and process algebra. In contrast to previous exercises (e.g., [1]), the system's description is an actual industrial standard which is being used to develop the next generation of automatic banking machines. The specification language Csp-Casl is particularly well suited to this type of problem, since it combines both control and data aspects and allows loose specification of data types for later refinement. During the formalisation, several inconsistencies and ambiguities were exhibited. The obtained specification serves as a starting point for further validation. [ABSTRACT FROM AUTHOR]

In previous work we gave an operational semantics and adequacy theorem for algebraic effects in programming languages. This covered finitary algebraic operations, thereby accommodating ordinary and probabilistic nondeterminism, output, and exceptions (but without handling), together with their combinations. With some extra effort, infinitary operations can also be covered, thereby also accommodating input and state. However one does not thereby obtain the natural operational semantics for state, which employs configurations of programs and states. We propose instead to consider the natural coalgebra of states given by the and operations; this coalgebra is the final comodel of the Lawvere theory for state. We therefore give an account integrating coalgebras given by comodels of Lawvere theories into the algebraic theory of effects. The coalgebras are used for the dynamics of the state component of the configurations. [ABSTRACT FROM AUTHOR]