相关论文: Logic Column 19: Symbolic Model Checking for Tempo…

We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then…

Justification logics are modal-like logics with the additional capability of recording the reason, or justification, for modalities in syntactic structures, called justification terms. Justification logics can be seen as explicit…

Many complex scenarios require the coordination of agents possessing unique points of view and distinct semantic commitments. In response, standpoint logic (SL) was introduced in the context of knowledge integration, allowing one to reason…

Model checking is a powerful technique for software verification. However, the approach notably suffers from the infamous state space explosion problem. To tackle this, in this paper, we introduce a novel symbolic method for encoding Petri…

Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics,…

Applying automated reasoning tools for decision support and analysis in law has the potential to make court decisions more transparent and objective. Since there is often uncertainty about the accuracy and relevance of evidence,…

A new logic for verification of security policies is proposed. The logic, HyperLTL, extends linear-time temporal logic (LTL) with connectives for explicit and simultaneous quantification over multiple execution paths, thereby enabling…

In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called…

We show that the model-checking problem is decidable for a fragment of the epistemic \mu-calculus. The fragment allows free variables within the scope of epistemic modalities in a restricted form that avoids constructing formulas embodying…

Integrating symbolic knowledge and data-driven learning algorithms is a longstanding challenge in Artificial Intelligence. Despite the recognized importance of this task, a notable gap exists due to the discreteness of symbolic…

Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and…

A modal logic based on quantum logic is formalized in its simplest possible form. Specifically, a relational semantics and a sequent calculus are provided, and the soundness and the completeness theorems connecting both notions are…

We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal…

This short note proposes a symbolic approach for representing and reasoning about quantum circuits using complex, vector or matrix-valued Boolean expressions. A major benefit of this approach is that it allows us to directly borrow the…

We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to characterise with STL formulae the input/output behaviour of…

Conditional independence reasoning has been shown to be helpful in the context of Bayesian nets to optimize probabilistic inference, and related techniques have been applied to speed up a number of logical reasoning tasks in boolean logic…

The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time…

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two…

We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value lambda-calculus. For this…

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep…