We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.

As they are conventionally formulated, Boolean games assume that players make their choices in ignorance of the choices being made by other players – they are games of simultaneous moves. For many settings, this is clearly unrealistic. In this paper, we show how Boolean games can be enriched by dependency graphs which explicitly represent the informational dependencies between variables in a game. More precisely, dependency graphs play two roles. First, when we say that variable x depends on variable y, then (...) we mean that when a strategy assigns a value to variable x, it can be informed by the value that has been assigned to y. Second, and as a consequence of the first property, they capture a richer and more plausible model of concurrency than the simultaneous-action model implicit in conventional Boolean games. Dependency graphs implicitly define a partial ordering of the run-time events in a game: if x is dependent on y, then the assignment of a value to y must precede the assignment of a value to x; if x and y are independent, however, then we can say nothing about the ordering of assignments to these variables—the assignments may occur concurrently. We refer to Boolean games with dependency graphs as partial-order Boolean games. After motivating and presenting the partial-order Boolean games model, we explore its properties. We show that while some problems associated with our new games have the same complexity as in conventional Boolean games, for others the complexity blows up dramatically. We also show that the concurrency in partial-order Boolean games can be modelled using a closure-operator semantics, and conclude by considering the relationship of our model to Independence-Friendly logic. (shrink)

In this paper, a timed modal logic L c is presented for the specification and verification of real-time systems. Several important results for L c are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for L c model checking. Finally we consider several control (...) problems for which L c can be used to check controllability. (shrink)

The book is about logical analysis of natural language. Since we humans communicate by means of natural language, we need a tool that helps us to understand in a precise manner how the logical and formal mechanisms of natural language work. Moreover, in the age of computers, we need to communicate both with and through computers as well. Transparent Intensional Logic is a tool that is helpful in making our communication and reasoning smooth and precise. It deals with all kinds (...) of linguistic context in a fully compositional and anti-contextual way. (shrink)

We introduce a new way of defining metric temporal logic on a real-numbers flow of time. The idea is based on having semantics which allow us to refer to a single universal clock of arbitrary precision in order to impose metric constraints. This gives us a new metric temporal logic which is very expressive, is natural to use, can be applied in very general situations, affords a wide range of useful abbreviations and operators, has a PSPACE decision procedure, and has (...) the promise of being amenable to standard reasoning techniques. Thus it has many advantages over the existing metric temporal logics. We provide a decision procedure via conversion to a non-metric temporal logic, hence doing metric reasoning with no clocks. (shrink)

ABSTRACT Most theorem provers for Classical Logic transform the input formula into a particular normal form. This tranformation is done before the execution of the algorithm or it is integrated into the deductive algorithm. This situation is no different for Non-Classical Logics and, particularly, for Temporal Logics. However, unlike classical logic, temporal logic does not provide an extension of the notion of non negative normal form. In this work, we define a temporal negative normal form for the future fragment of (...) the linear time propositional temporal logic, named FNext. The definition saves as much information as possible about implicants and implicates of the input formula and its subformulas. This property is the novelty of this normal form; for example, in [Fis97] the normal form is guided by the separation property and in [Ven86] the normal form provided prepares the input formula to be treated by a resolution method. Moreover, we also introduce an algorithm having linear cost, which transforms the input formula into a temporal negative normal form. Furthermore, in this work we present a new structure and a set of operators over it that allows us to efficiently manage the information about unitary implicants and implicates contained in the subformulae. (shrink)

We define bisimulations for temporal logic with Since and Until. This new notion is compared to existing notions of bisimulations, and then used to develop the basic model theory of temporal logic with Since and Until. Our results concern both invariance and definability. We conclude with a brief discussion of the wider applicability of our ideas.

Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we (...) propose a selection of landmark results about decidability, complexity and expressive power. (shrink)

Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.