Search

Abstract: Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers and determine sup and inf over all paths from a given state, and the temporal operators and specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the -calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics. [Copyright &y& Elsevier]

Abstract: We extend the logic for abstract state machines by a read predicate that allows to make precise statements about the accesses of locations of an ASM. The logic can be used to prove security properties of ASMs like that the machine does not read locations containing critical information or that all accesses of the machine to the abstract memory are permitted. The new read predicate is also useful for proving refinements of parallel ASMs to sequential C-like programs. The logic is complete for hierarchical ASMs and still sound for turbo ASMs. It is integrated in the ASMKeY theorem prover. [Copyright &y& Elsevier]

Abstract: We study structural properties of each of the main sublanguages of navigational XPath (W3c Recommendation) commonly used in practice. First, we characterize the expressive power of these language fragments in terms of both logics and tree patterns. Second, we investigate closure properties, focusing on the ability to perform basic Boolean operations while remaining within the fragment. We give a complete picture of the closure properties of these fragments, treating XPath expressions both as functions of arbitrary nodes in a document tree, and as functions that are applied only at the root of the tree. Finally, we provide sound and complete axiom systems and normal forms for several of these fragments. These results are useful for simplification of XPath expressions and optimization of XML queries. [Copyright &y& Elsevier]

Abstract: Multitree are unranked, unordered trees and occur in many Computer Science applications like rewriting and logic, knowledge representation, XML queries, typing for concurrent systems, cryptographic protocols, etc. We define constrained multitree automata which accept sets of multitrees where the constraints are expressed in a first-order theory of multisets with counting formulas which is very expressive. We give constructions for union, intersection, determinization. Then, we give an algorithm to decide emptiness when the constraints belong to a subclass where counting is limited to distinct elements. We show that many classes of tree automata that have been defined for a wide variety of applications can be seen as instance of our general framework. Finally, we describe the quantifier elimination procedure used to decide the theory of constraints. [Copyright &y& Elsevier]

Abstract: The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula. This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) the sp equivalence for the so-called locally-independent ntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems, (2) verification for locally-independent processes and negation-free first-order formulae of the ntcc LTL, (3) implication for such formulae, (4) Satisfiability for a first-order fragment of Manna and Pnueli''s LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency. [Copyright &y& Elsevier]

Abstract: The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering new forms of reasoning: the local reasoning through the separation of the resource space into two disjoint subspaces, and the contextual reasoning through hypothetical extension of the resource space. We consider two resource models and their related logics:[] The static ambient model, proposed as an abstraction of semistructured data (Proc. ESOP’01, Lecture Notes in Computer Science, vol. 2028, Springer, Berlin, 2001, pp. 1–22 (invited paper)) with the static ambient logic (SAL) that was proposed as a request language, both obtained by restricting the mobile ambient calculus (Proc. FOSSACS’98, Lecture Notes in Computer Science, vol. 1378, Springer, Berlin, 1998, pp. 140–155) and logic (Proc. POPL’00, ACM Press, New York, 2000, pp. 365–377) to their purely static aspects. [] The memory model and the assertion language of separation logic, both defined in Reynolds (Proc. LICS’02, 2002) for the purpose of the axiomatic semantic of imperative programs manipulating pointers. We raise the questions of the expressiveness and the minimality of these logics. Our main contribution is a minimalisation technique we may apply for these two logics. We moreover show some restrictions of this technique for the extension with universal quantification, and we establish the minimality of the adjunct-free fragment (). [Copyright &y& Elsevier]

Abstract: We present a compositional approach to defining expressive logics for coalgebras of endofunctors on . This approach uses a notion of language constructor and an associated notion of semantics to capture one inductive step in the definition of a language for coalgebras and of its semantics. We show that suitable choices for the language constructors and for their associated semantics yield logics which are both adequate and expressive w.r.t. behavioural equivalence. Moreover, we show that type-building operations give rise to corresponding operations both on language constructors and on their associated semantics, thus allowing the derivation of expressive logics for increasingly complex coalgebraic types. Our framework subsumes several existing approaches to defining logics for coalgebras, and at the same time allows the derivation of new logics, with logics for probabilistic systems being the prime example. [Copyright &y& Elsevier]

Both Kripke models and interpreted systems have been put forward as basic models of multi-agent systems and for reasoning about Knowledge in such systems. This paper enriches previous comparisons of these two forms of semantics by considering categories of models in both cases and then shows that constructions given by Lomuscio and Ryan, extend to give an adjoint equivalence between the two settings. This equivalence is exploited in a discussion of colimits of interpreted systems. [Copyright &y& Elsevier]

We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment. [Copyright &y& Elsevier]

In this paper we study the recognizability and definability on existential monadic second order (EMSO) logic of languages related to homogeneous flow event structures (HFES), i.e., the languages of configurations (posets) and the languages of proving sequences (words).An HFES is specified by an arbitrary poset G = (V,⩽) and a finite FES F as a result of copying F in vertices of G with additional homogeneous flow and conflict relations on the events of adjacent vertices.The problem is: whether the sets of configurations of HFES and languages of proving sequences are EMSO-definable.Results refer to the domains of linear orders, binary trees, and two-dimensional grids. If G is the domain of linear order or binary tree then the recognizability and EMSO-definability of configurations of HFES hold. We give some classes of HFES where the recognizability does not hold for the two-dimensional grid.The EMSO-definability of proving sequences is proved for all considered classes of HFES. [Copyright &y& Elsevier]

An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Gödel''s T and therefore defines a non-size-increasing polynomial time computable function. [Copyright &y& Elsevier]

It is well known that one can build models of full higher-order dependent-type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra. But the idea of categories of PERs and ERs (total equivalence relations) can be applied to other structures as well. In particular, we can easily define the category of ERs and equivalence-preserving continuous mappings over the standard category Top0 of topological T0-spaces; we call these spaces (a topological space together with an ER) equilogical spaces and the resulting category Equ. We show that this category—in contradistinction to Top0—is a cartesian closed category. The direct proof outlined here uses the equivalence of the category Equ to the category PEqu of PERs over algebraic lattices (a full subcategory of Top0 that is well known to be cartesian closed from domain theory). In another paper with Carboni and Rosolini (cited herein), a more abstract categorical generalization shows why many such categories are cartesian closed. The category Equ obviously contains Top0 as a full subcategory, and it naturally contains many other well known subcategories. In particular, we show why, as a consequence of work of Ershov, Berger, and others, the Kleene–Kreisel hierarchy of countable functionals of finite types can be naturally constructed in Equ from the natural numbers object N by repeated use in Equ of exponentiation and binary products. We also develop for Equ notions of modest sets (a category equivalent to Equ) and assemblies to explain why a model of dependent type theory is obtained. We make some comparisons of this model to other, known models. [Copyright &y& Elsevier]

This paper gives some new logical characterizations of the class of rudimentary languages in the scope of descriptive complexity. These characterizations are based on a logic introduced by Parigot and Pelz to characterize Petri Net languages, and generalized quantifiers of comparison of cardinality. [Copyright &y& Elsevier]

The LA-logics (“logics with Local Agreement”) are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov''s logic DALLA and Nakamura''s logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively. [Copyright &y& Elsevier]

Sharing graphs are an implementation of linear logic proof-nets in which a redex is never duplicated. In their usual formulation, sharing graphs present a problem of coherence: if the proof-net N reduces by standard cut-elimination to N′, then, by reducing the sharing graph of N we do not obtain the sharing graph of N′. We solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). The rewriting system is confluent and terminating. The proof exploits an algebraic semantics for sharing graphs. [Copyright &y& Elsevier]

The motivating role of linear logic is as a “logic behind logic”. We propose a sibling role for it as a logic of transformational mathematics via the self-dual category of Chu spaces, a generalization of topological spaces. These create a bridge between linear logic and mathematics by soundly and fully completely interpreting linear logic while fully and concretely embedding a comprehensive range of concrete categories of mathematics. Our main goal is to treat each end of this bridge in expository detail. In addition, we introduce the dialectic lambda-calculus, and show that dinaturality semantics is not fully complete for the Chu interpretation of linear logic. [Copyright &y& Elsevier]

Intuitionistic and linear logics can be used to specify the operational semantics of transition systems in various ways. We consider here two encodings: one uses linear logic and maps states of the transition system into formulas, and the other uses intuitionistic logic and maps states into terms. In both cases, it is possible to relate transition paths to proofs in sequent calculus. In neither encoding, however, does it seem possible to capture properties, such as simulation and bisimulation, that need to consider all possible transitions or all possible computation paths. We consider augmenting both intuitionistic and linear logics with a proof theoretical treatment of definitions. In both cases, this addition allows proving various judgments concerning simulation and bisimulation (especially for noetherian transition systems). We also explore the use of infinite proofs to reason about infinite sequences of transitions. Finally, combining definitions and induction into sequent calculus proofs makes it possible to reason more richly about properties of transition systems completely within the formal setting of sequent calculus. [Copyright &y& Elsevier]

It is well known that every proof net of a non-commutative version of MLL (multiplicative fragment of commutative linear logic) can be drawn as a plane Danos–Regnier graph (drawing) satisfying the switching condition of Danos–Regnier . In this paper, we study the reverse direction; we introduce a system MNCLL which is logically equivalent to the multiplicative fragment of cyclic linear logic introduced by Yetter , and show that any plane Danos–Regnier graph drawing with one terminal edge satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL). In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planarity, as well as the notion of a certain long-trip condition, called the stack-condition, of a Danos–Regnier graph, the latter of which is related to Abrusci''s balanced long-trip condition . [Copyright &y& Elsevier]

Light linear logic (Girard, Inform. Comput. 14 (1998) 175–204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely semantic proof of cut elimination as a consequence. A number of mathematical examples of fibred phase spaces are presented that illustrate subtleties of light linear logic. [Copyright &y& Elsevier]

We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property. [Copyright &y& Elsevier]

‘Almost-certain eventualities’ are liveness properties that hold with probability 1. ‘Abstract probabilities’ in transition systems are those known only to be bounded away from zero and one.Vardi (Proceedings of the 26th IEEE Symposium on Foundations of Computer Science, Portland, 1985, p. 327) showed that almost-certain properties in linear temporal logic depend only on abstract probabilities rather than on the probabilities’ precise values. We discuss the extent to which a similar result holds in the quantitative temporal logic qTL derived from the quantitative modal μ-calculus qMμ (Proceedings the Formal Methods Pacific ’97, Springer, Singapore, 1997, also available http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html; logic J, IGPL 7(6) (1999) 779, http://www3.oup.co.uk/igp1/Volume_07/Issue_06, http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html), and we show how to specialise the logic to these cases. The aim is to provide a simpler calculus than the full logic, one that is in a certain sense complete for proving almost-certain eventualities from abstract-probabilistic assumptions.We conclude by considering the complexity of the specialised logic. [Copyright &y& Elsevier]

The primary objective of this paper is to present the definition of a new dynamic, linear and modal logic for security protocols. The logic is compact, expressive and formal. It allows the specification of classical security properties (authentication, secrecy and integrity) and also electronic commerce properties (non-repudiation, anonymity, good atomicity, money atomicity, certified delivery, etc.). The logic constructs are interpreted over a trace-based model. Traces reflect valid protocol executions in the presence of a malicious smart intruder. The logic is endowed with a tableau-based proof system that leads to a modular denotational semantics and local model checking. [Copyright &y& Elsevier]

This paper presents an object-oriented model for broadband telecommunication networks, which can be used both for network management and for network planning purposes. The object-oriented model has been developed using the parallel object-oriented specification language Maude, which allows us to define not only structural aspects of the model but also procedural aspects. The reflective properties of rewriting logic are applied to control the rewriting process, using a strategy language that can be specified internally to the logic. Several modeling approaches are compared, emphasizing the definition of the object relationships and the benefits obtained from using reflection as opposed to the extra effort required to control the process at the object level itself. [Copyright &y& Elsevier]

This paper explores the application of rewriting logic to the executable formal modeling of real-time and hybrid systems. We give general techniques by which such systems can be specified as ordinary rewrite theories, and show that a wide range of real-time and hybrid system models, including object-oriented systems, timed automata, hybrid automata, timed and phase transition systems, and timed extensions of Petri nets, can indeed be expressed in rewriting logic quite naturally and directly. Since rewriting logic is executable and is supported by several language implementations, our approach complements property-oriented methods and tools less well suited for execution purposes, and can be used as the basis for symbolic simulation and formal analysis of real-time and hybrid systems. The relationships with the timed rewriting logic approach of Kosiuczenko and Wirsing are also studied. [Copyright &y& Elsevier]

In addition to equations and rules, we introduce equational rules that are oriented while having an equational interpretation. Correspondence between operational behavior and intended semantics is guaranteed by a property of coherence, which can be checked by examination of critical pairs and linearity conditions. We present applications of this theory to three examples where the rewrite relation is interpreted, respectively, as equality, transition and deduction. [Copyright &y& Elsevier]

The large diffusion of concurrent and distributed systems has spawned in recent years a variety of new formalisms, equipped with features for supporting an easy specification of such systems. The aim of our paper is to analyze three proposals, namely rewriting logic, action calculi and tile logic, chosen among those formalisms designed for the description of rule-based systems. For each of these logics we first try to understand their foundations, then we briefly sketch some applications. The overall goal of our work is to find out a common layout where these logics can be recast, thus allowing for a comparison and an evaluation of their specific features. [Copyright &y& Elsevier]

We recall general metalogical axioms for a reflective logic based on the notion of a universal theory, that is, a theory that can simulate the deductions of all other theories in a class of theories of interest, including itself. We then show that conditional rewriting logic is reflective, generalizing in two stages: first to the unsorted conditional case, and then to the many-sorted conditional case, the already known result for unconditional and unsorted rewriting logic (Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, 2000). This work should be seen as providing foundations for many useful applications of rewriting logic reflection. The results presented here have greatly influenced the design of the Maude language, which implements rewriting logic and supports its reflective capabilities, and have been used as a theoretical foundation for applications such as internal rewrite strategies, reflective design of theorem proving tools, module algebra and metaprogramming, and metareasoning in metalogical frameworks. [Copyright &y& Elsevier]

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude''s language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude. [Copyright &y& Elsevier]

ELAN implements computational systems, a concept that combines two first class entities: rewrite rules and rewriting strategies. ELAN can be used either as a logical framework or to describe and execute deterministic as well as non-deterministic rule-based processes. With the general goal to make precise a rewriting logic-based semantics of ELAN, this paper has three contributions: a presentation of the concepts of rules and strategies available in ELAN, an expression of rewrite rules with matching conditions in conditional rewriting logic, and finally an enrichment mechanism of a rewrite theory into a strategy theory in conditional rewriting logic. [Copyright &y& Elsevier]

The variety of semantical approaches that have been invented for logic programs is quite broad, drawing on classical and many-valued logic, lattice theory, game theory, and topology. One source of this richness is the inherent non-monotonicity of its negation, something that does not have close parallels with the machinery of other programming paradigms. Nonetheless, much of the work on logic programming semantics seems to exist side by side with similar work done for imperative and functional programming, with relatively minimal contact between communities. In this paper we summarize one variety of approaches to the semantics of logic programs: that based on fixpoint theory. We do not attempt to cover much beyond this single area, which is already remarkably fruitful. We hope readers will see parallels with, and the divergences from the better known fixpoint treatments developed for other programming methodologies. [Copyright &y& Elsevier]

A main task in document transformation and information retrieval is locating subtrees satisfying some pattern. Therefore, unary queries, i.e., queries that map a tree to a set of its nodes, play an important role in the context of structured document databases. The motivation of this work is to understand how the natural and well-studied computation model of tree automata can be used to compute such queries. We define a query automaton (QA) as a deterministic two-way finite automaton over trees that has the ability to select nodes depending on the state and the label at those nodes. We study QAs over ranked as well as over unranked trees. Unranked trees differ from ranked ones in that there is no bound on the number of children of nodes. We characterize the expressiveness of the different formalisms as the unary queries definable in monadic second-order logic (MSO). In contrast to the ranked case, special stay transitions had to be added to QAs over unranked trees to capture MSO. We establish the complexity of the non-emptiness, containment, and equivalence of QAs to be complete for EXPTIME. [Copyright &y& Elsevier]

This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR). [Copyright &y& Elsevier]