Search

This paper introduces Graded Computation Tree Logic with finite path semantics (GCTL f ⁎ , for short), a variant of Computation Tree Logic CTL⁎, in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTL f ⁎ are interpreted over Kripke structures. The syntax of GCTL f ⁎ has path quantifiers of the form E ≥ g ψ which express that there are at least g many distinct finite paths that satisfy ψ. After defining and justifying the logic GCTL f ⁎ , we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTL f ⁎ under the imperfect information setting. Precisely, we introduce GCTLK f ⁎ , an epistemic extension of GCTL f ⁎ and prove that the model checking problem also in this case is PSPACE-complete. [ABSTRACT FROM AUTHOR]

We study a variant ATL FB of the alternating-time temporal logic ATL with a non-standard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL FB differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL FB. The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL FB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL FB and prove its soundness and completeness. [ABSTRACT FROM AUTHOR]

In Temporal Logic (TL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions , are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed since their equivalent concise syntax formulas can be found. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax by means of fixed-point approach. Firstly, we present two kinds of formulas, namely ⋁ i ∈ N 0 ◯ i Q and ⋁ i ∈ N 0 Q i , and prove they are indeed well-formed by proving they are equivalent to formulas ◇ Q and Q ⁎ respectively. Further, we generalize ⋁ i ∈ N 0 ◯ i Q to ⋁ i ∈ N 0 P (i) ∧ ◯ i Q and explore the least and greatest fixed-points of an abstract equation X ≡ Q ∨ P ∧ ◯ X. Based on these, some well-formed special instances of ⋁ i ∈ N 0 P (i) ∧ ◯ i Q are obtained. Besides, with the index set expression technique, we equivalently represent ' U ' (strong until) and ' W ' (weak until) constructs of propositional Linear Temporal Logic (LTL) within Propositional Projection Temporal Logic (PPTL). [ABSTRACT FROM AUTHOR]

We introduce a new concept in the area of formal logic: axioms for model morphisms. We work in the setting of specification languages that define the semantics of a theory as a category of models. While it is routine to use axioms to specify the class of models of a theory, there has so far been no analogue to systematically specify the morphisms between these models. This leads to subtle problems where it is difficult to give a theory that specifies the intended model category, or where seemingly isomorphic theories actually have non-isomorphic model categories. Our morphism axioms remedy this by providing new syntax for axiomatizing and reasoning about the properties of model morphisms. Additionally, our system resolves a subtle incompatibility between theory morphisms and model morphisms: the semantics that maps theories to model categories is functorial. While this result is standard in principle, previous formulations had to restrict the allowed theory morphisms or the allowed model morphisms. Our system allows establishing the result in full generality. [ABSTRACT FROM AUTHOR]

Although there have been many works on bounded semantics, a characterization of a good definition for a bounded semantics has not been given, and this has led to definitions of bounded semantics of temporal logics that may not be appropriate with respect to the potential usefulness as a basis for developing bounded model checking approaches. On the other side, the research effort on bounded semantics has mainly focused on existentially interpreted fragments of temporal logics, due to the intricacy of defining appropriate bounded semantics for universally interpreted fragments, or for temporal logics with path quantifiers that are closed under negation. This work addresses these two problems, by defining the characteristics of bounded semantics for clarifying the concept of bounded semantics, and presenting a bounded semantics for the full set of CTL, a logic closed under negation, including possibility for specifying both existential and universal properties. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we consider the robust interpretation of Metric Temporal Logic (MTL) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, , from unsatisfiability. We prove that any other signal that remains -close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely Metric Interval Temporal Logic (MITL) and closed Metric Temporal Logic (clMTL), over continuous-time signals using only discrete-time analysis. The motivating idea behind our approach is that if the continuous-time signal fulfills certain conditions and the discrete-time signal robustly satisfies the temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification. [Copyright &y& Elsevier]

Abstract: Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one. Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. In this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution. [Copyright &y& Elsevier]

Abstract: The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network. [Copyright &y& Elsevier]

Abstract: Commutative, integral and bounded -algebras form a subvariety of residuated lattices which provides the algebraic semantics of an interesting common fragment of intuitionistic logic and of several fuzzy logics. It is known that both the equational theory and the quasiequational theory of commutative -algebras are decidable (in contrast to the noncommutative case), but their complexity has not been studied yet. In this paper, we prove that both theories are in , and that the quasiequational theory is -hard. [Copyright &y& Elsevier]

Abstract: We develop possible worlds (Kripke) semantics at the categorical abstract model theoretic level provided by the so-called ‘institutions’. Our general abstract modal logic framework provides a method for systematic Kripke semantics extensions of logical systems from computing science and logic. We also extend the institution-independent method of ultraproducts of [R. Diaconescu, Institution-independent ultraproducts, Fundamenta Informaticæ 55 (3–4) (2003) 321–348] to possible worlds semantics and prove a fundamental preservation result for abstract modal satisfaction. As a consequence we develop a generic compactness result for possible worlds semantics. [Copyright &y& Elsevier]

Abstract: We present a trace semantics for a language of parallel programs which share access to mutable data. We introduce a resource-sensitive logic for partial correctness, based on a recent proposal of O’Hearn, adapting separation logic to the concurrent setting. The logic allows proofs of parallel programs in which “ownership” of critical data, such as the right to access, update or deallocate a pointer, is transferred dynamically between concurrent processes. We prove soundness of the logic, using a novel “local” interpretation of traces which allows accurate reasoning about ownership. We show that every provable program is race-free. [Copyright &y& Elsevier]

Abstract: The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be difficult to reason about because of being inherently non-modular. We argue that this is untrue. We take it seriously that, unlike statements of a high-level language, pieces of low-level code are multiple-entry and multiple-exit. And we define a piece of code as consisting of either a single labelled instruction or a finite union of pieces of code. Thus we obtain a compositional natural semantics and a matching Hoare logic for a basic low-level language with jumps. By their simplicity and intuitiveness, these are comparable to the standard natural semantics and Hoare logic of While. The Hoare logic is sound and complete wrt the semantics and allows for compilation of proofs of the Hoare logic of While. [Copyright &y& Elsevier]

Abstract: Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory’s axioms include both equations and rewrite rules provides a useful “abstraction dial” to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities. [Copyright &y& Elsevier]

Abstract: In this paper we compare the semantical and syntactical definitions of extensions for open default theories. We prove that, over monadic languages, these definitions are equivalent and do not depend on the cardinality of the underlying infinite world. We also show that, under the domain closure assumption, one free variable open default theories are decidable. [Copyright &y& Elsevier]

Abstract: Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications. [Copyright &y& Elsevier]

Abstract: Periodicity constraints are used in many logical formalisms, in fragments of Presburger LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic , an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a PSPACE-complete satisfiability problem, we establish that model-checking and satisfiability problems remain in PSPACE as plain LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to , EXPSPACE-complete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is PSPACE-complete by designing a reduction from QBF and by using our results for . [Copyright &y& Elsevier]

Abstract: Full first-order linear logic can be presented as an abstract logic programming language in Miller''s system Forum, which yields a sensible operational interpretation in the ‘proof search as computation’ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first-order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system. [Copyright &y& Elsevier]

Abstract: We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of where subscripts put quantitative constraints on the time it takes before a property is satisfied. We exhibit an important gap between logics where subscripts of the form “” (exact duration) are allowed, and simpler logics that only allow subscripts of the form “” or “” (bounded duration). Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes -complete or -complete depending on the considered semantics. [Copyright &y& Elsevier]

Abstract: We are interested in separation-logic-based static analysis of programs that use shared mutable data structures. In this paper, we introduce backward and forward analysis for a separation logic called , an extension of separation logic [Ishtiaq and O’Hearn, BI as an assertion language for mutable data structures, in: POPL’01, 2001, pp. 14–26], to which we add fixpoint connectives and postponed substitution. This allows us to express recursive definitions within the logic as well as the axiomatic semantics of while statements. [Copyright &y& Elsevier]

Abstract: In UML 2.0 sequence diagrams have been considerably extended but their expressiveness and semantics remains problematic in several ways. In other work we have shown how sequence diagrams combined with an OCL liveness template gives us a much richer language for inter-object behaviour specification. In this paper, we give a semantics of these enriched diagrams using labelled event structures. Further, we show how sequence diagrams can be embedded into a true-concurrent two-level logic interpreted over labelled event structures. The top level logic, called communication logic, is used to describe inter-object specification, whereas the lower level logic, called home logic, describes intra-object behaviour. An interesting consequence of using this logic relates to how state-based behaviour can be synthesised from inter-object specifications. Plans of extending the Edinburgh Concurrency Workbench in this context are discussed. [Copyright &y& Elsevier]

Abstract: We consider the multiplicative and exponential fragment of linear logic (MELL) and give a geometry of interaction (GoI) semantics for it based on unique decomposition categories. We prove a soundness and finiteness theorem for this interpretation. We show that Girard''s original approach to GoI 1 via operator algebras is exactly captured in this categorical framework. [Copyright &y& Elsevier]