CoCasl at Work — Modelling Process Algebra

CoCasl[11], a recently developed coalgebraic extension of the algebraic specification language Casl[2], allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS[10] and CSP[8,17], within such an algebraic-coalgebraic framework. It turns out that CoCasl can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structural operational semantics fit well in the algebraic world of Casl, while the additional coalgebraic constructs of CoCasl cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains. CoCasl hence becomes a meta-framework for studying the semantics and proof theory of reactive systems.     

Automata and fixed point logic: A coalgebraic perspective

This paper generalizes existing connections between automata and logic to a coalgebraic abstraction level. Let F: Set to Set be a standard functor that preserves weak pullbacks. We introduce various notions of F-automata, devices that operate on pointed F-coalgebras. The criterion under which such an automaton accepts or rejects a pointed coalgebra is formulated in terms of an infinite two-player graph game. We also introduce a language of coalgebraic fixed point logic for F-coalgebras, and we provide a game semantics for this language. Finally, we show that the two approaches are equivalent in expressive power. We prove that any coalgebraic fixed point formula can be transformed into an F-automaton that accepts precisely those pointed F-coalgebras in which the formula holds. And conversely, we prove that any F-automaton can be converted into an equivalent fixed point formula that characterizes the pointed F-coalgebras accepted by the automaton.     

A refinement-based process algebra for timed automata

We propose a real-time extension to the process algebra CSP. Inspired by timed automata, a very successful formalism for the specification and verification of real-time systems, we handle real time by means of clocks, i.e. real-valued variables that increase at the same rate as time. This differs from the conventional approach based on timed transitions. We give a discrete trace and failures semantics to our language and define the resulting refinement relations. One advantage of our proposal is that it is possible to automatically verify refinement relations between processes. We demonstrate how this can be achieved and under which conditions.Partially supported by EPSRC grant GR/N22960.Received January 2004Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

An approach for machine-assisted verification of Timed CSP specifications

The real-time process calculus Timed CSP is capable of expressing properties such as deadlock-freedom and real-time constraints. It is therefore well-suited to model and verify embedded software. However, proofs about Timed CSP specifications are not ensured to be correct since comprehensive machine-assistance for Timed CSP is not yet available. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. This allows for semi-automated and mechanically checked proofs about Timed CSP specifications. Mechanically checked proofs enhance confidence in verification because corner cases cannot be overlooked. We additionally apply our formalization to an abstract specification with real-time constraints. This is the basis for our current work, in which we verify a simple real-time operating system deployed on a satellite. As this operating system has to cope with arbitrarily many threads, we use verification techniques from the area of parameterized systems for which we outline their formalization.     

A Coalgebraic Approach to Kleene Algebra with Tests

Kleene Algebra with Tests is an extension of Kleene Algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene Algebra with Tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene Algebra with Tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene Algebra with Tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene Algebra with Tests expressions.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

Optimization by a Team of Independent Automata with Adaptation

This paper continues our work [1-3] on the search and optimization capabilities of teams of independent automata. We shall present numerical data on some mechanisms of adaptation of optimizing automata. These mechanisms represent attempts to overcome the basic contradiction, inherent in any search system, between the desire to maximize the speed of search for the proper action (i.e., minimize the number of purposeless actions) and the desire to maintain a sufficiently large repertoire of such actions. Such attempts, induced by biological associations, involve the introduction of inhibitions and excitations that are produced by the system itself in response to its estimate of the effect of these actions (this estimate can be termed emotional), and also the introduction of the estimates (which accumulate during the operation of the system) of the individual automata taking part in the process.     

Subsequential transducers: a coalgebraic perspective

Subsequential transducers combine (input) language recognition with transduction and thereby generalise classic deterministic automata as well as Mealy and Moore type state machines. These well known subclasses all have a natural coalgebraic characterisation, and the question arises whether their coalgebraic modelling can be extended to subsequential transducers and their underlying structures. In this paper, we show that although subsequential structures cannot generally be regarded as coalgebras, the subclass of normalised structures do form a subcategory of coalgebras. Moreover, normalised structures are reflective in the category of all subsequential structures, and a final normalised structure exists. The existence and properties of the minimal subsequential transducer can be derived from this result. We also show that for the class of subsequential structures in which all states are accepting, an alternative coalgebraic representation is obtained by taking differentials. This differential representation gives rise to a new method of deciding equivalence and computing minimal representations which does not involve normalisation. Both normalisation and taking differentials can be formalised as functors into reflective subcategories of coalgebras, and we can therefore see these constructions as coalgebraisation.     

General control systems

In this paper we propose a model for interaction between random environments and random automata. To this model we can apply the theory of (generalized) random systems with complete connections (i.e., learning models or dynamic models) in order to describe its behavior. We shall call such a system a general control system. Next criteria and conditions of expediency of a random automaton within such a system are formulated. Finally two special cases are examined.     

Marker automata

This paper deals with finite automata augmented with markers which the automata can move about on their input tapes. The concept of augmenting markers to automata was first introduced by Blum and Hewitt [1] in two-dimensional automata. Kreider, Ritchie, and Springsteel [6, 7, 8, 12] investigated recognition of context-free languages by (one-dimensional) automata with markers. In this paper, we investigate some fundamental properties of marker automata and study their relationships to other types of automata and languages. The main result in this paper is the establishment of an infinite hierarchy of languages recognizable by deterministic and deterministic, halting marker automata. It also turns out that, because of the equivalence of finite marker automata and multi-head automata, the study of three-marker automata becomes very interesting due to results of Hartmanis [4] and Savitch [10].     

Collective Behavior of G-Type Automata

The adaptive capabilities of automata are judged primarily on the basis of their behavior in random environments (situations). One can, of course, study these properties from various points of view, but the ability of automata to participate in games, i.e., their purposive collective behavior, is of special interest. This means that we have a ν-person game, the players being given not only the rules of the game, but also any other information that may be useful, such as the strategies of all the participants. It is assumed that if this game admits a behavior which is most advantageous for all the players (“the game has a solution”), then the competent and reasonable participants will adopt this behavior.     

Model checking probabilistic systems against pushdown specifications

Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are non-regular. For instance, requirements which involve counting cannot be formalized by regular specifications but using pushdown specifications, i.e., context-free properties represented by pushdown automata. Research on model-checking techniques for pushdown specifications is, however, rare and limited to the verification of non-probabilistic systems.In this paper, we address the probabilistic model-checking problem for systems modeled by discrete-time Markov chains and specifications that are provided by deterministic pushdown automata over infinite words. We first consider finite-state Markov chains and show that the quantitative and qualitative model-checking problem is solvable via a product construction and techniques that are known for the verification of probabilistic pushdown automata. Then, we consider recursive systems modeled by probabilistic pushdown automata with an infinite-state Markov chain semantics. We first show that imposing appropriate compatibility (visibility) restrictions on the synchronizations between the pushdown automaton for the system and the specification, decidability of the probabilistic model-checking problem can be established. Finally we prove that slightly departing from this compatibility assumption leads to the undecidability of the probabilistic model-checking problem, even for qualitative properties specified by deterministic context-free specifications.     

Resolution approach to testing compatibility of interacting automata

Conclusion The notion of compatibility of automata was proposed in [1] for formalization of requirements that must be met by interacting partial automata. Testing the compatibility of automata is of essential importance for the design of systems that interact with the environment, especially when we use declarative specificatio of the system to be designed. Under the assumptions of this article for the automaton that models the environment, partiality of the specified automaton is a source of possible incompatibility with the environment. When declarative specification is used, we can never decide in advance if the specified automaton is partial or not. Moreover, even a specification thata priori describes a completely defined automaton may be altered by the actions of the designer in the process of design (especially if these actions are incorrect) so that the specified automaton becomes partial. Therefore the initial specification, and each successive specification produced by human intervention in the design process, must be tested for compatibility with the environment. In the methodology of verification design of automata, compatibility testing is used to solve two problems: a) generating the specification of the class of all automata that satisfy the initial specification and are compatible with the specification of the environment; b) testing for correctness the designer's decisions that alter the current specification of the automaton being designed. The results of this article have led to the development of an efficient resolution procedure for testing the compatibility of automaton specification with the specification of the environment. this procedure has been implemented in the system for verification design of automata from their logical specifications. The efficiency of the developed procedure is based on the results of compatibility analysis of automata from [1] and on the restricted resolution strategy whose completeness and correctness have been proved in [2]. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 36–50, November–December, 1994.     

Generating Processes from Specifications using the Relation Manipulation System RelView

In this paper we present an algorithm generating a bundle of processes from a given safety specification. The specification is given by a formula in a process logic, i.e. a modal logic with a set of possibility operators induced by the possible actions of the underlying transition system. This logic is a finite sublanguage, in the sense that only finite conjunctions are allowed, of the language introduced by R. Milner in [3]. Furthermore, we present an implementation of the algorithm using the functional language HASKELL and the internal language of the RelView system. Within the system processes are modelled by relations as shown in [8,9].     

Semantic business process integration based on ontology alignment

Innovation and agility should be provided to businesses by efficient collaboration (i.e., communication and sharing) between them. However, semantic heterogeneity between business processes is a serious problem for automatically supporting cooperation processes (e.g., knowledge sharing and querying-based interactions) between businesses. In order to overcome this problem, we propose a novel framework based on aligning business ontologies for integrating heterogeneous business processes. We can consider two types of alignment processes; (i) manual alignment for building a whole business process ontology in a business process management (BPM) system and (ii) automated alignment between business processes of different BPM systems. Thereby, the optimal integration between two business processes has to be discovered to maximize the summation of a set of partial similarities between semantic components consisting of the business processes. In particular, the semantic component are extracted from semantic annotations of business processes. For evaluating the proposed system, we have conducted experimentations by using 22 business process management systems, which are organized as six business alliances. We have assumed that business processes in a same BPM system should be built with a common ontologies. The proposed alignment method has shown about 71.3% of precision (65.4% of recall). In addition, we found out that alignment results are dependent on some characteristics of ontologies (e.g., depth and number of classes).     

Engineering constraint solvers for automatic analysis of probabilistic hybrid automata

In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata [33]. Generalizing SMT-based bounded model-checking of hybrid automata [5], [31], stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.     

Controller synthesis for dynamic hierarchical real-time plants using timed automata

We use timed I/O automata based timed games to synthesize task-level reconfiguration services for cost-effective fault tolerance in a case study. The case study shows that state-space explosion is a severe problem for timed games. By applying suitable abstractions, we dramatically improve the scalability. However, timed I/O automata do not facilitate algorithmic abstraction generation techniques. The case study motivates the development of timed process automata to improve modeling and analysis for controller synthesis of time-critical plants which can be hierarchical and dynamic. The model offers two essential features for industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating plant processes which can activate other plant processes. We show how to establish safety and reachability properties of timed process automata by reduction to solving timed games. To mitigate the state-space explosion problem, an algorithmic state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed. In this article, we demonstrate the theoretical framework of timed process automata and the effectiveness of the proposed state-space reduction technique by extending the case study.     

Revisiting the security of secure direct communication based on ping-pong protocol[Quantum Inf. Process. 8, 347 (2009)]

A. Chamoli and C.M. Bhandari presented a secure direct communication based on ping-pong protocol[Quantum Inf. Process. 8, 347 (2009)]. M.Naseri analyzed its security and pointed out that in this protocol any dishonest party can obtain all the other one’s secret message with zero risk of being detected by using fake entangled particles (FEP attack) [M. Naseri, Quantum Inf. Process. online]. In this letter, we reexamine the protocol’s security and discover that except the FEP attack, using a special property of GHZ states, any one dishonest party can also take a special attack, i.e., double-CNOT(Controlled NOT) attack. Finally, a denial-of-service attack is also discussed.     

Toward a boundary regional control problem for Boolean cellular automata

An important question to be addressed regarding system control on a time interval [0, T] is whether some particular target state in the configuration space is reachable from a given initial state. When the target of interest refers only to a portion of the spatial domain, we speak about regional analysis. Cellular automata approach have been recently promoted for the study of control problems on spatially extended systems for which the classical approaches cannot be used. An interesting problem concerns the situation where the subregion of interest is not interior to the domain but a portion of its boundary . In this paper we address the problem of regional controllability of cellular automata via boundary actions, i.e., we investigate the characteristics of a cellular automaton so that it can be controlled inside a given region only acting on the value of sites at its boundaries.