Search

In a period-timestamped, relational temporal database, each tuple is timestamped with a period. The timestamp records when the tuple is "alive" in some temporal dimension. Sequenced semantics is a special semantics for evaluating a query in a temporal database. The semantics stipulates that the query must, in effect, be evaluated simultaneously in each time instant using the tuples alive at that instant. Previous research has proposed changes to a database management system's query evaluation engine to support sequenced semantics. We show how to achieve sequenced semantics without modifying a query evaluation engine. Our technique has two pillars. First we use log-segmented timestamps to record a tuple's lifetime. A log-segmented timestamp divides the time-line into segments of known length. Any temporal period can be represented by a small number of such segments. Second, by taking advantage of the properties of log-segmented timestamps, we translate a sequenced query to a non-temporal query, using the operations already present in an unmodified, non-temporal query evaluation engine. The paper provides translations for both relational algebra and SQL. We experimentally evaluate the SQL translation. The primary contribution of this paper is how to implement sequenced semantics using log-segmented timestamped tuples in a generic SQL DBMS. [ABSTRACT FROM AUTHOR]

Abstract: In this paper we summarise Safe, a first-order functional language for programming small devices and embedded systems with strict memory requirements, which has been introduced elsewhere. It has some unusual memory management features such as heap regions and explicit cell deallocation. It is targeted at a Proof Carrying Code environment, and consistently with this aim the Safe compiler provides machine checkable certificates about important safety properties such as the absence of dangling pointers and bounded memory consumption. The kernel of the paper is devoted to developing part of the Safe compiler's back-end, by deriving an appropriate abstract machine from the language semantics, by providing the code generation functions, and by formally proving that the translation is sound, both in the semantic and in the memory consumption senses. [Copyright &y& Elsevier]

Abstract: “Clarithmetic” is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their “truth” is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic. [Copyright &y& Elsevier]

Abstract: Deterministic behavior for parallel and distributed computation is rather difficult to ensure. To reach that goal, many formal calculi, languages, and techniques with well-defined semantics have been proposed in the past. But none of them focused on an imperative object calculus with asynchronous communications and futures. In this article, an object calculus, Asynchronous Sequential Processes (ASP), is defined, with its semantics. We prove also confluence properties for the ASP calculus. ASPs main characteristics are asynchronous communications with futures, and sequential execution within each process. This paper provides a very general and dynamic property ensuring confluence. Further, more specific and static properties are derived. Additionally, we present a formalization of distributed components based on ASP, and show how such components are used to statically ensure determinacy. This paper can also be seen as a formalization of the concept of futures in a distributed object setting. [Copyright &y& Elsevier]

Abstract: This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles. [Copyright &y& Elsevier]

Abstract: Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules. We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning. [Copyright &y& Elsevier]

Abstract: This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. [Copyright &y& Elsevier]

Information integration systems provide uniform interfaces to varieties of heterogeneous information sources. For query answering in such systems, the current generation of query answering algorithms in local-as-view (source-centric) information integration systems all produce what has been thought of as “the best obtainable” answer, given the circumstances that the source-centric approach introduces incomplete information into the virtual global relations. However, this “best obtainable” answer does not include all information that can be extracted from the sources because it does not allow partial information. Neither does the “best obtainable” answer allow for composition of queries, meaning that querying a result of a previous query will not be equivalentto the composition of the two queries. In this paper, we provide a foundation for information integration, based on the algebraic theory of incomplete information. Our framework allows us to define the semantics of partial facts and introduce the notion of the exact answer—that is the answer that includes partial facts. We show that querying under the exact answer semantics is compositional. We also present two methods for actually computing the exact answer. The first method is tableau-based, and it is a generalization of the “inverse-rules” approach. The second, much more efficient method, is a generalization of the rewriting approach, and it is based on partial containment mappings introduced in the paper. [Copyright &y& Elsevier]

Earlier we presented a method to decompose modal formulas for processes with the internal action τ , and congruence formats for branching and η -bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality 〈 ϵ 〉 〈 a 〉 φ , to derive congruence formats for delay and weak bisimilarity. [ABSTRACT FROM AUTHOR]

Interval order structures are useful tools to model abstract concurrent histories, i.e. sets of equivalent system runs, when system runs are modeled with interval orders . This paper shows how interval order structures can be modeled by partially commutative monoids , called interval traces . The model is then used to provide a semantics of Petri nets with inhibitor arcs, both in terms of interval traces and in terms of interval order structures. [ABSTRACT FROM AUTHOR]

In learning, a semantic or behavioral U-shape occurs when a learner first learns, then unlearns, and, finally, relearns, some target concept. This paper introduces two general techniques and applies them especially to syntactic U-shapes in learning: one technique to show when they are necessary and one to show when they are unnecessary. The technique for the former is very general and applicable to a much wider range of learning criteria. It employs so-called self-learning classes of languages which are shown to characterize completely one criterion learning more than another. We apply these techniques to show that, for set-driven and rearrangement-independent learning, any kind of U-shapes is unnecessary. Furthermore, we show that U-shapes are necessary in a strong way for iterative learning, contrasting with an earlier result by Case and Moelius that semantic U-shapes are un necessary for iterative learning. [ABSTRACT FROM AUTHOR]

Classical results in computability theory, notably Rice's theorem, focus on the extensional content of programs, namely, on the partial recursive functions that programs compute. Later work investigated intensional generalisations of such results that take into account the way in which functions are computed, thus affected by the specific programs computing them. In this paper, we single out a novel class of program semantics based on abstract domains of program properties that are able to capture nonextensional aspects of program computations, such as their asymptotic complexity or logical invariants, and allow us to generalise some foundational computability results such as Rice's Theorem and Kleene's Second Recursion Theorem to these semantics. In particular, it turns out that for this class of abstract program semantics, any nontrivial abstract property is undecidable and every decidable over-approximation necessarily includes an infinite set of false positives which covers all the values of the semantic abstract domain. [ABSTRACT FROM AUTHOR]

With an aim to developing expressive language theoretical tools applicable to inverse semigroup languages, that is, subsets of inverse semigroups, this paper explores the language theory of finite labeled birooted trees: Munn's birooted trees extended with vertex labeling. To this purpose, we define a notion of finite state birooted tree automata that simply extends finite state word automata semantics. This notion is shown to capture the class of languages that are definable in Monadic Second Order Logic and upward closed with respect to the natural order. Then, we derive from these automata the notion of quasi-recognizable languages, that is, languages recognizable by means of (adequate) premorphisms into finite (adequately) ordered monoids. This notion is shown to capture finite Boolean combinations of languages as above, a class that contains classical regular languages of finite (mono-rooted) trees. This contrasts with the known collapse of classical algebraic tools when applied to inverse semigroups. [ABSTRACT FROM AUTHOR]

Abstract: The assumption of being able to perform infinite precision measurements does not only lead to undecidability, but it also introduces artifacts in the mathematical models that do not correspond to observable behaviours of systems under study. When bounded spatial regions are involved, such issues can be avoided if arbitrarily small sets of points are not definable in the mathematical setting. ϵ-semantics were introduced in this spirit. In this paper we investigate the use of ϵ-semantics deeper, in the context of reachability analysis of hybrid automata. In particular, we focus on two ϵ-semantics and reason about their computability. We then try our approach on biological model analysis to give evidence about the effectiveness of the methodology. [Copyright &y& Elsevier]

Abstract: This paper investigates the stochastic, continuous and instantaneous (hybrid) modelling of systems defined in Bio-PEPA, a quantitative process algebra for biological modelling. This is achieved by mapping a Bio-PEPA model to a model in stochastic HYPE, a process algebra that models these three behaviour types in a compositional and structured manner. The novel mapping between process algebras provides another method of analysis for Bio-PEPA models and presents the modeller with a well-structured stochastic HYPE model which can itself be easily modified and is only a small constant larger in size than the Bio-PEPA model. The structure of the stochastic HYPE model generated has desirable properties and also gives a general framework for modelling biochemical systems where the advantages of both stochastic and deterministic simulation are required. Thresholds are introduced for each reaction, and when all values are above these thresholds, the reaction is treated deterministically. However, if a relevant value is below a threshold, the reaction is treated stochastically (as are the changes in species quantities as a result of that reaction). It is proved that in the purely deterministic case and in the purely stochastic case, the stochastic HYPE model has the same behaviour as the Bio-PEPA model when considered purely deterministically and purely stochastically, respectively. Furthermore, addition of instantaneous events in the style of Bio-PEPA with events is illustrated, and a proposal for mapping Bio-PEPA with delays (Bio-PEPAd) to stochastic HYPE is presented. [Copyright &y& Elsevier]

Abstract: Least upper bounds play an important role in defining the semantics of programming languages, and in abstract interpretations. In this paper, we identify conditions on countable ordered measurable spaces that ensure the existence of least upper bounds for all sets of probability measures. These conditions are shown to be necessary as well — for any measurable space not satisfying these conditions, there are (finite) sets of probability measures for which no least upper bound exists. For measurable spaces meeting these conditions, the existence of least upper bounds is established constructively. Based on this least upper bound construction, we present a novel abstraction method applicable to Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of the new abstraction techniques is that the resulting abstract models are purely probabilistic that may be more amenable to automated analysis than models with both nondeterministic and probabilistic transitions which arise from previously known abstraction techniques. [Copyright &y& Elsevier]

Abstract: In this paper we present what is thought to be the worldʼs shortest correct exact real arithmetic program. The aim is to provide a tractable starting point for formal analysis and further development. In addition the program presented here allows beginners to the field to easily experiment with a practical implementation in order to understand some of the issues involved. The algorithms used have been validated using PVS which provides some grounds for believing them to be correct. However, as neither PVS nor Haskell have been similarly validated, semantic problems in either PVS or Haskell might still undermine the work. A slightly shorter program with the same functionality could be written, but there would be a significant degradation in performance. By performing better range reduction, the performance could be increased. However, we would lose the correctness proofs and the program would become a bit longer and even more opaque. [Copyright &y& Elsevier]

Abstract: In this paper, we introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the -calculus, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the -calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature. [Copyright &y& Elsevier]

Abstract: Partial transition systems support abstract model checking of complex temporal properties by combining both over- and under-approximating abstractions into a single model. Over the years, three families of such modeling formalisms have emerged, represented by (1) Kripke Modal Transition Systems (KMTSs), with restrictions on necessary and possible behaviors; (2) Mixed Transition Systems (MixTSs), with relaxation on these restrictions; and (3) Generalized Kripke MTSs (GKMTSs), with hyper-transitions, respectively. In this paper, we investigate these formalisms based on two fundamental ways of using partial transition systems (PTSs) – as objects for abstracting concrete systems (and thus, a PTS is semantically consistent if it abstracts at least one concrete system) and as models for checking temporal properties (and thus, a PTS is logically consistent if it gives consistent interpretation to all temporal logic formulas). We study the connection between semantic and logical consistency of PTSs, compare the three families w.r.t. their expressive power (i.e., what can be modeled, what abstractions can be captured using them), and discuss the analysis power of these formalisms, i.e., the cost and precision of model checking. Specifically, we identify a class of PTSs for which semantic and logical consistency coincide and define a necessary and sufficient structural condition to guarantee consistency. We also show that all three families of PTSs have the same expressive power (but do differ in succinctness). However, GKMTSs are more precise (i.e., can establish more properties) for model checking than the other two families. The direct use of GKMTSs in practice has been hampered by the difficulty of encoding them symbolically. We address this problem by developing a new semantics for temporal logic of PTSs that makes the MixTS family as precise for model checking as the GKMTS family. The outcome is a symbolic model checking algorithm that combines the efficient encoding of MixTSs with the model checking precision of GKMTSs. Our preliminary experiments indicate that the new algorithm is a good match for predicate-abstraction-based model checkers. [Copyright &y& Elsevier]

Abstract: Inspired by the classical theory of modules over a monoid, we introduce the natural notion of module over a monad. The associated notion of morphism of left modules (“linear” natural transformations) captures an important property of compatibility with substitution, not only in the so-called homogeneous case but also in the heterogeneous case where “terms” and variables therein could be of different types. In this paper, we present basic constructions of modules and we show how modules allow a new point of view concerning higher-order syntax and semantics. [Copyright &y& Elsevier]

Abstract: Categorial grammars in the tradition of Lambek are asymmetric: sequent statements are of the form , where the succedent is a single formula A, the antecedent a structured configuration of formulas . The absence of structural context in the succedent makes the analysis of a number of phenomena in natural language semantics problematic. A case in point is scope construal: the different possibilities to build an interpretation for sentences containing generalized quantifiers and related expressions. In this paper, we explore a symmetric version of categorial grammar, based on work by Grishin . In addition to the Lambek product, left and right division, we consider a dual family of type-forming operations: coproduct, left and right difference. Communication between the two families is established by means of structure-preserving distributivity principles. We call the resulting system LG. We present a Curry-Howard interpretation for LG derivations, based on Curien and Herbelin’s lambda mu comu calculus. We discuss continuation-passing-style (CPS) translations mapping LG derivations to proofs/terms of Intuitionistic Multiplicative Linear Logic — the categorial system LP which serves as the logic for natural language meaning assembly. We show how LG, thus interpreted, associates sentences with quantifier phrases with the appropriate range of meanings, thus overcoming the expressive limitations of asymmetric categorial grammars in this area. [Copyright &y& Elsevier]

Abstract: The paper proposes a novel analysis of quantificational subordination, e.g., Harvey courts a woman at every convention.She is very pretty. vs. She always comes to the banquet with him. — in particular of the fact that the indefinite in the initial sentence can have wide or narrow scope, but the first discourse as a whole allows only for the wide scope reading, while the second discourse allows for both readings. The cross-sentential interaction between scope and anaphora is captured in terms of structured anaphora to quantifier domains, formalized in a new dynamic system couched in classical type logic that builds on the Dynamic Plural Logic of van den Berg . Given the underlying type logic, compositionality at sub-clausal level follows automatically. Modal subordination is analyzed in a parallel way, thereby capturing the parallels between the individual and modal domains repeatedly argued for in the literature. We also outline the analysis of several other phenomena in terms of structured anaphora: exceptional scope, weak/strong donkey readings, anaphoric/uniqueness-implying definite descriptions and interactions between same / different and quantifier scope. [Copyright &y& Elsevier]

Abstract: Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations. [Copyright &y& Elsevier]

Abstract: Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion. In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences. [Copyright &y& Elsevier]

Abstract: Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results. [Copyright &y& Elsevier]

Abstract: This paper investigates both the precision and the model checking efficiency of abstract models designed to preserve branching time logics w.r.t. a 3-valued semantics. Current abstract models use ordinary transitions to over approximate the concrete transitions, while they use hyper transitions to under approximate the concrete transitions. In this work, we refer to precision measured w.r.t. the choice of abstract states, independently of the formalism used to describe abstract models. We show that current abstract models do not allow maximal precision. We suggest a new class of models and a construction of an abstract model which is most precise w.r.t. any choice of abstract states. As before, the construction of such models might involve an exponential blowup, which is inherent by the use of hyper transitions. We therefore suggest an efficient algorithm in which the abstract model is constructed during model checking, by need. Our algorithm achieves maximal precision w.r.t. the given property while remaining quadratic in the number of abstract states. To complete the picture, we incorporate it into an abstraction-refinement framework. [Copyright &y& Elsevier]

Abstract: Van Glabbeek presented the linear time–branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek’s axiomatizations that they are -complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time–branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is -complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions. [Copyright &y& Elsevier]

Abstract: Several attempts have been made of extending to graph grammars the unfolding semantics originally developed by Winskel for (safe) Petri nets, but only partial results were obtained. In this paper, we fully extend Winskel’s approach to single-pushout grammars providing them with a categorical concurrent semantics expressed as a coreflection between the category of (semi-weighted) graph grammars and the category of prime algebraic domains, which factorises through the category of occurrence grammars and the category of asymmetric event structures. For general, possibly nonsemi-weighted single-pushout grammars, we define an analogous functorial concurrent semantics, which, however, is not characterised as an adjunction. Similar results can be obtained for double-pushout graph grammars, under the assumptions that nodes are never deleted. [Copyright &y& Elsevier]

Abstract: Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with λ-abstraction, etc.). We show that Constraint LTL over the simple domain augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes -completeness. On the positive side, we provide complexity results when the domain is finite (ExpSpace-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSpace and ExpSpace). [Copyright &y& Elsevier]

Abstract: 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. [Copyright &y& Elsevier]

Abstract: Cousot and Cousot introduced and studied a general past/future-time specification language, called ▪-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the ▪-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete, that is trace-incom-plete, even for finite systems. As a consequence, standard state-based model checking of the ▪-calculus is incomplete w.r.t. trace-based model checking. This paper shows that any refinement or abstraction of the domain of sets of states induces a corresponding semantics which is still trace-incomplete for any propositional fragment of the ▪-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the ▪-calculus, that characterize the structure of models, i.e., transition systems, whose corresponding state-based semantics of the ▪-calculus is trace-complete. [Copyright &y& Elsevier]

Abstract: This paper is devoted to probabilistic models for concurrent systems under their true-concurrency semantics. Here we address probabilistic event structures. We consider a new class of event structures, called locally finite, that extend confusion-free event structure. In locally finite event structures, maximal configurations can be tiled with branching cells: branching cells are minimal and finite sub-structures capturing the choices performed while scanning a maximal configuration. The probabilistic event structures that we introduce have the property that “concurrent processes are independent in the probabilistic sense.” [Copyright &y& Elsevier]

Abstract: When a process is capable of executing an unbounded number of non-observable actions it is said to be divergent. Different capabilities of an observer to identify this phenomena along the execution leads to different divergent sensitive semantics. This paper develops sound and complete axiomatisations for the divergence sensitive spectrum of weak bisimulation equivalence. The axiomatisations separates the axioms concerning recursion and those that capture the essence of diverging behaviour. [Copyright &y& Elsevier]

This paper presents persistent Turing machines (PTMs), a new way of interpreting Turing-machine computation, based on dynamic stream semantics. A PTM is a Turing machine that performs an infinite sequence of “normal” Turing machine computations, where each such computation starts when the PTM reads an input from its input tape and ends when the PTM produces an output on its output tape. The PTM has an additional worktape, which retains its content from one computation to the next; this is what we mean by persistence.A number of results are presented for this model, including a proof that the class of PTMs is isomorphic to a general class of effective transition systems called interactive transition systems; and a proof that PTMs without persistence (amnesic PTMs) are less expressive than PTMs. As an analogue of the Church-Turing hypothesis which relates Turing machines to algorithmic computation, it is hypothesized that PTMs capture the intuitive notion of sequential interactive computation. [Copyright &y& Elsevier]

The verification of programs that contain mutually recursive procedures is a difficult task, and one which has not been satisfactorily addressed in the literature. Published proof rules have been later discovered to be unsound. Verification condition generator (VCG) tools have been effective in partially automating the verification of programs, but in the past these VCG tools have in general not themselves been proven, so any proof using and depending on these VCGs might not be sound. In this paper, we present a set of proof rules for proving the partial correctness of programs with mutually recursive procedures, together with a VCG that automates the use of the proof rules in program correctness proofs. The soundness of the proof rules and the VCG itself have been mechanically proven within the Higher Order Logic theorem prover, with respect to the underlying structural operational semantics of the programming language. This proof of soundness then forms the core of an implementation of the VCG that significantly eases the verification of individual programs with complete security. [Copyright &y& Elsevier]

Intersection types discipline allows to define a wide variety of models for the type free lambda-calculus, but the Curry–Howard isomorphism breaks down for this kind of type systems. In this paper we show that the correspondence between types and suitable logical formulas can still be recovered appealing to the fact that there is a strict connection between the semantics for lambda-calculus induced by the intersection types and a Kripke-style semantics for modal and relevant logics. Indeed, we present a modal logic hinted by the analysis of the sub-typing relation for intersection types, and we show that the deduction relation for such a modal system is a conservative extension of the relation of sub-typing. Then, we define a Kripke-style semantics for the formulas of such a system, present suitable sequential calculi, prove a completeness theorem and give a syntactical proof of the cut elimination property. Finally, we define a decision procedure for theorem-hood and we show that it yields the finite model property and cut-redundancy. [Copyright &y& Elsevier]

In categorical semantics, there have traditionally been two approaches to modelling environments, one by use of finite products in cartesian closed categories, the other by use of the base categories of indexed categories with structure. Each requires modifications in order to account for environments in call-by-value programming languages. There have been two more general definitions along both of these lines: the first generalising from cartesian to symmetric premonoidal categories, the second generalising from indexed categories with specified structure to κ-categories. In this paper, we investigate environments in call-by-value languages by analysing a fine-grain variant of Moggi’s computational λ-calculus, giving two equivalent sound and complete classes of models: one given by closed Freyd categories, which are based on symmetric premonoidal categories, the other given by closed κ-categories. [Copyright &y& Elsevier]

Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i.e., transparent to object clients. In previous work, we introduced Ø, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used Ø in order to exhibit how the semantics behind Obliq''s implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of Ø in terms of the π-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Ø. [Copyright &y& Elsevier]

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in π -calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible π -calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible π -calculus causal semantics. [ABSTRACT FROM AUTHOR]

This paper contributes to a generic theory of behaviour of "finite-state" systems. Systems are coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to the locally finite fixpoint (LFF), a new fixpoint of the endofunctor. The LFF exists provided that the endofunctor is finitary and preserves monomorphisms, is a subcoalgebra of the final coalgebra, i.e. it is fully abstract w.r.t. behavioural equivalence, and it is characterized by two universal properties: as the final locally finitely generated coalgebra, and as the initial fg-iterative algebra. Instances of the LFF are: regular languages, rational streams, rational formal power-series, regular trees etc. Moreover, we obtain e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S -algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten), and the monad of Courcelle's algebraic trees. [ABSTRACT FROM AUTHOR]

In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a τ -transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of τ -transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart. [ABSTRACT FROM AUTHOR]