Related papers: Temporal Stream Logic modulo Theories (Full Versio…

In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded…

We continue the investigation of parameterized extensions of Linear Temporal Logic (LTL) that retain the attractive algorithmic properties of LTL: a polynomial space model checking algorithm and a doubly-exponential time algorithm for…

This paper addresses the problem of data-driven model discrimination for unknown switched systems with unknown linear temporal logic (LTL) specifications, representing tasks, that govern their mode sequences, where only sampled data of the…

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time…

Humans continuously make new discoveries, and understanding temporal sequence of events leading to these breakthroughs is essential for advancing science and society. This ability to reason over time allows us to identify future steps and…

Signal Temporal Logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog com- ponents. STL…

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…

CTL is the dominant temporal specification language in practice mainly due to the fact that it admits model checking in linear time. Logic programming and the database query language Datalog are often used as an implementation platform for…

Learning to solve complex tasks with signal temporal logic (STL) specifications is crucial to many real-world applications. However, most previous works only consider fixed or parametrized STL specifications due to the lack of a diverse STL…

We extend Signal Temporal Logic (STL) to enable the specification of importance and priorities. The extension, called Weighted STL (wSTL), has the same qualitative (Boolean) semantics as STL, but additionally defines weights associated with…

We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but additionally allows to use high level constructs, such as…

In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted…

The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and…

We introduce and investigate a number of fragments of propo- sitional temporal logic LTL over the flow of time (Z, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of…

Providing adequate tools to tackle the problem of inconsistent compliance rules is a critical research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of…

Large Language Models (LLMs) still struggle with complex logical reasoning. While previous works achieve remarkable improvements, their performance is highly dependent on the correctness of translating natural language (NL) problems into a…

Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of…

We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e.,…

This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The…

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…