Journal: ACM Transactions on Computational Logic

Abbreviation

ACM trans. comput. log.

Publisher

Association for Computing Machinery

Journal Volumes

ISSN

1529-3785
1557-945X

Description

Filters

Reset filters

Search Results

Publications1 - 7 of 7
  • A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
    Item type: Journal Article
    Matheja, Christoph; Pagel, Jens; Zuleger, Florian (2023)
    ACM Transactions on Computational Logic
    We develop a doubly exponential decision procedure for the satisfiability problem of guarded separation logic - a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the preceding connectives leads to an undecidable fragment.We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly exponential decision procedure for entailments between (quantifier-free) symbolic heaps with inductive predicate definitions of bounded treewidth (SLbtw) - one of the most expressive decidable fragments of separation logic. Together with the recently shown 2ExpTime-hardness for entailments in said fragment, we conclude that the entailment problem for SLbtw is 2ExpTime-complete - thereby closing a previously open complexity gap.
  • Bounds on the automata size for Presburger arithmetic
    Item type: Journal Article
    Klaedtke, Felix (2008)
    ACM Transactions on Computational Logic
    Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by the automata-based approach for Presburger arithmetic. In this article, we give an upper bound on the number of states of the minimal deterministic automaton for a Presburger arithmetic formula. This bound depends on the length of the formula and the quantifiers occurring in it. We establish the upper bound by comparing the automata for Presburger arithmetic formulas with the formulas produced by a quantifier-elimination method. We show that our bound is tight, also for nondeterministic automata. Moreover, we provide automata constructions for atomic formulas and establish lower bounds for the automata for linear equations and inequations.
  • Reflective Metalogical Frameworks
    Item type: Journal Article
    Basin, David; Clavel, Manuel; Meseguer, Jose (2004)
    ACM Transactions on Computational Logic
    A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be good metalogical frameworks when their theories always have initial models and they support reflective and parameterized reasoning.We develop this thesis both abstractly and concretely. Abstractly, we formalize our proposal as a set of requirements and explain how any logic satisfying these requirements can be used for metalogical reasoning. Concretely, we present membership equational logic as a particular metalogic that satisfies these requirements. Using membership equational logic, and its realization in the Maude system, we show how reflection can be used for different, nontrivial kinds of formal metatheoretic reasoning. In particular, one can prove metatheorems that relate theories or establish properties of parameterized classes of theories.
  • A Theory of Sampling for Continuous-Time Metric Temporal Logic
    Item type: Journal Article
    Furia, Carlo A.; Rossi, Matteo (2010)
    ACM Transactions on Computational Logic
    This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to “flat” formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete time, resulting in an automated partial practically efficient discretization technique.
  • Modal Abstractions of Concurrent Behavior
    Item type: Journal Article
    Nielson, Flemming; Nanz, Sebastian; Nielson, Hanne Riis (2011)
    ACM Transactions on Computational Logic
    We present an effective algorithm for the automatic construction of finite modal transition systems as abstractions of potentially infinite concurrent processes. Modal transition systems are recognized as valuable abstractions for model checking because they allow for the validation as well as refutation of safety and liveness properties. However, the algorithmic construction of finite abstractions from potentially infinite concurrent processes is a missing link that prevents their more widespread usage for model checking of concurrent systems. Our algorithm is a worklist algorithm using concepts from abstract interpretation and operating upon mappings from sets to intervals in order to express simultaneous over- and underapproximations of the multisets of process actions available in a particular state. We obtain a finite abstraction that is 3-valued in both states and transitions and that supports the definition of a 3-valued modal logic for validating as well as refuting properties of systems. The construction is illustrated on a few examples, including the Ingemarsson-Tang-Wong key agreement protocol.
  • Runtime verification over out-of-order streams
    Item type: Journal Article
    Basin, David; Klaedtke, Felix; Zălinescu, Eugen (2019)
    ACM Transactions on Computational Logic
    We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach handles an expressive specification language that extends the real-time logic MTL with freeze quantifiers for reasoning about data values. The logic’s main novelty is a new three-valued semantics that is well suited for runtime verification as it accounts for partial knowledge about a system’s behavior. Based on this semantics, we present online algorithms that reason soundly and completely about streams where events can occur out of order. We also evaluate our algorithms experimentally. Depending on the specification, our prototype implementation scales to out-of-order streams with hundreds to thousands of events per second.
  • Deciding security properties for cryptographic protocols
    Item type: Journal Article
    Comon-Lundh, Hubert; Cortier, Véronique; Zălinescu, Eugen (2010)
    ACM Transactions on Computational Logic
    There is a large amount of work dedicated to the formal verification of security protocols. In this article, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint to a set of solved forms, representing all solutions (within the bound on sessions). As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k, k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required. We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.
Publications1 - 7 of 7