相关论文: A History of Until

We consider an extension of linear-time temporal logic (LTL) with both local and remote data constraints interpreted over a concrete domain. This extension is a natural extension of constraint LTL and the Temporal Logic of Repeating Values,…

Primarily guided with the idea to express zero-time transitions by means of temporal propositional language, we have developed a temporal logic where the time flow is isomorphic to ordinal $\omega^2$ (concatenation of $\omega$ copies of…

The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual…

This article examines the interpretation of the LTL temporal operators over finite and infinite sequences. This is used as the basis for deriving a sound and complete axiomatization for Caret, a recent temporal logic for reasoning about…

The paper studies problems of satisfiability, decidability and admissibility of inference rules, conceptions of knowledge and agent's knowledge in non-transitive temporal linear logic LTL(Past,m). We find algorithms solving mentioned…

Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only…

We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considering queries formulated in fragments of propositional linear…

We combine linear temporal logic (with both past and future modalities) with a deontic version of justification logic to provide a framework for reasoning about time and epistemic and normative reasons. In addition to temporal modalities,…

We consider G\"odel temporal logic ($\sf GTL$), a variant of linear temporal logic based on G\"odel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a…

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable…

While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound…

Lewis' theory of counterfactuals is the foundation of many contemporary notions of causality. In this paper, we extend this theory in the temporal direction to enable symbolic counterfactual reasoning on infinite sequences, such as…

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free…

In this paper we propose a many-valued temporal conditional logic. We start from a many-valued logic with typicality, and extend it with the temporal operators of the Linear Time Temporal Logic (LTL), thus providing a formalism which is…

Temporal reasoning in dynamic, data-intensive environments increasingly demands expressive yet tractable logical frameworks. Traditional approaches often rely on negation to express absence or contradiction. In such contexts,…

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem…

It is shown that the decision problem for the temporal logic with until and since connectives over real-numbers time is PSPACE-complete.

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for…

Sound and complete axiomatizations are provided for a number of different logics involving modalities for knowledge and time. These logics arise from different choices for various parameters. All the logics considered involve the discrete…

Defeasible logic is a rule-based nonmonotonic logic, with both strict and defeasible rules, and a priority relation on rules. We show that inference in the propositional form of the logic can be performed in linear time. This contrasts…