An Overview of Temporal Logic at Advanced Course of Applied Logics at Tallinn University of Technology

This week was prominent because of a mandatory assignment being completed at university. An overview of Temporal logic was a duty for Advanced Course of Applied Logics. A common notion of a logic is explained. A formal grammar and a difference of expressiveness is addressed. Application techniques and fields for utilization are specified.

Logic is a formal or informal system based on principles of valid and correct reasoning, proceeding from statements (expressions), which were asserted, to those, which were derived and inferred. If it is an informal system, natural language is the assumption and consequently the reasoning method is inductive at most cases. Such a reasoning is drawing certain conclusions from specific examples and observations. As opposite to, the deductive reasoning is also utilized. Because this method is drawing logical conclusions from existing definitions and formal inference rules, a formal system is usually assumed. Consequently, Temporal logic as a formal logic system is demonstrated in this overview.

To start with, if a formal logic is demonstrated, its formal grammar is explained. A formal grammar defines atoms as basic units and well-formed formulas, which are utilized for obtaining further recursively units, well-formed formulas or formulas. It is expressed with the ability of logical (for example, operators) and non-logical (for example, variables) symbols. Formulas are well-formed formulas, because these are defined in terms of a formal grammar. The precise form of a formal grammar depends on a formal logic under consideration. Each logic is characterized by its own proper traits.

Before Temporal logic is turned to, it is necessary to clarify that Propositional logic is not comparable with Aristotle’s logic based on syllogisms. Because the former is a part of a modern logical system, whereas the latter is a part of the oldest logical system. However, both utilize the same principle as one proposition (a conclusion) being inferred from other propositions (premises). If this principle is developed further with a certain form, the formation of propositions from propositions being compared to a sequence of state transitions can particularly refer to the passage as anticipation of Temporal logic.

Temporal logic is the branch of a formal logic, which allows to express and reason about concepts of time. It is formed by adding temporal operators to an existed logic, for example, to Propositional or Predicate logic. Concepts of time are expressed by various sequences of state transitions. As for this logic being formal, it has a formal grammar which defines atoms as basic units and a notion of a well-formed formula. Propositional logic and Predicate as First-order logic are demonstrated for being extended to temporal logic only by adding temporal operators. In this case, it is obvious that a formal grammar of it will depend on those being extended. Atoms of Propositional logic are (primitive symbols) simple propositions called well-formed formulas as well as atoms of First-order logic are (variables, functions) terms. While the precise specifics of a definition of atomic units and well-formed formulas depends on each logic separately, Temporal logic has it exactly as its one being extended, Propositional or First-order logic.

Following the explanation of a formal grammar of Temporal logic, it is concluded that this grammar consists of precise specifics as well as commonly utilized logical and just added temporal operators. A logical operator is a constant symbol, which can be utilized to connect not only two truth-value sentences (binary operator) but also a different number of truth-value sentences (n-ary operator) to one compound truth-value sentence. The addition of temporal operators to a grammar maintains notions of well-formed formulas practically unchanged, but defined further according to. If a formula was a well-formed formula, it remains to be well-formed with right utilization of a legitimate temporal operator. Temporal Logic as the branch has several subsets, but only quite a few are demonstrated. To this end, commonly implemented temporal operators are following:

f U g Until: until some future time (state)
X f Next: the next time (state)
F f Future: some next time (state)
G f Globally: all future time (states)

By now, it is necessary to clarify the difference between utilization of predicate and temporal quantifiers. In the case of a predicate quantifier, it can be the existential or universal quantifier, asserting that a formula holds for at least one or any members of a domain. The domain is a set of individual elements which can be quantified over. In the distinct case of a temporal quantifier, it is similar to a modal logic one for expressing possibility and necessity modalities referring to time, but in the exact case of temporal logic concepts of time are expressed by various sequences of state transitions. The utilization of predicate and temporal quantifiers allows to be referred to different objects existing at different times and expressed important distinctions of time and existence.

Linear temporal logic (LTL) is different from other subsets, it can reason about a single (sequential) time line. Earlier mentioned notions of well-formed formulas remain to be well-formed formulas as it was explained. Although LTL does not include additional operators to common ones, it is worth to emphasize that it is restricted to a linear structure.

Computational Tree logic (CTL) is an alternate formalism and views time as branching and discrete. It can reason about multiple time lines. As a consequence, new temporal operators are added to those mentioned earlier. The addition of new operators divides all temporal operators into groups of path-specific quantifiers and quantifiers over paths. The common temporal operators are brought to the group of path-specific quantifiers, whereas just added new ones fill the group of quantifiers over paths, and these are following:

A f Always: along all paths
E f Eventually: along at least one path

Every formula, which is formulated with all those appropriate operators of CTL, cannot be the same moment a CTL well-formed formula, because it follows a restricted set of formation rules. As for path-specific quantifiers and quantifiers over paths being separate groups of temporal operators of CTL, in its well-formed formula every path-specific quantifier must be preceded by a quantifier over path, must always be grouped in two. Although LTL can imply the quantifier over path A (Always), there are obviously formulas that are not both LTL and CTL formulas. LTL does not actually include quantifiers over path and can be expressed very differently without even considering this kind of quantifiers.

CTL* contains both LTL and CTL as its subsets. CTL* is similar to CTL, both implement basically the same path-specific quantifiers and quantifiers over paths. However, formation rules are not restricted and quantifiers can be freely mixed. As a result, CTL* is strictly more expressive than LTL and CTL.

Utilization of Temporal logic can be in many fields. This logic is formal for expressing concepts of time. If it is necessary to express those concepts by the formal and precise way in any field, possibilities of Temporal logic are for those purposes. In the context of utilization, the fields related to natural language and computer science are stressed.

Natural language can be thought of as an informal logic, but its certain scope can be formally expressed with the ability of Temporal logic. Natural language usually consists of, for example, past, present and future tenses. Special constructions exist in language, which allow to formulate tenses. Consequently, it is possible, for example, to formulate certain constructions and also analyze tenses of natural language. Although Temporal logic is formal, natural language is informal itself and can be very rich with tenses and expressions. Because expressions can be ambiguous, contextually dependent and erroneous, they also have different meanings in different communities, it may be problematic to cover an analysis thoroughly.

The field of computer science is especially stressed. In this field, Temporal logic is mainly concerned with a specification and verification of computer programs. Due to the fact that these days programs are less designed to execute on a single processor in a single process, concurrent programs are more stressed or those programs which are performed in parallel by processors. For those programs, it is necessary to formulate temporal components and on their basis to develop certain temporal models. As a consequence, Temporal logic is the most effective formalization for specifying and verifying those types of programs.

First of all, Temporal logic is utilized for a specification of a program. It is supposed that if a program is possessed, it is necessary to compose a documentation or a (formal) specification. A specification is a formal or informal description of functioning of a program. It may be informal by utilizing, for example, English for a description of what a program should do under certain conditions. Alternatively, it can be highly mathematical, utilizing a formalism defined for that purpose. The formalism of Temporal logic is for indicating temporal ingredients. A formal specification may be implied that this one is formally correct. In order to be confident, this formal specification is verified that a model based on it is following formalism rules, consistent and correct.

Then, if verification of a program is needed, the formalism of Temporal logic is also utilized. Additionally, not only a specification is composed but also a certain model is developed what is verified to be consistent and correct with respect to a specification. Because Temporal logic is expressed by sequences of state transitions, it is possible with this ability to verify state transitions of a particular object, for example, access to a resource. The specifics of verification depend on principles being applied. One principle is to verify behaviors for which a given model is valid. The other principle is to investigate at least one behavior for which the negation (of pre- and post-conditions) of a given model is satisfied. Model checking and logical inference are approaches to formal verification.

Model checking is an approach to exhaustive verification of a (mathematical) model. A model checker automatically verifies consistency and correctness requirements against a model. Those requirements are absence of deadlocks and other critical states that can cause a program to crash.

Logical inference, on the other hand, is an approach to development of new proofs and theorems, usually utilizing a theorem prover. A theorem prover attempts to demonstrate that premises and a conclusion are provably equivalent. For this reason, a theorem prover produces inference steps, taking into consideration premises. The proving is successful when finished with the conclusion that is a logical consequence from premises. A theorem prover implements a formalism for formulating formal logical conception. Mainly, it is assumed that first-order logic is the most common logical system a theorem prover deals with. When it is supposed and alternatively looked at, a certain formalism can be implemented for formulating temporal characteristics. Consequently in the course of the proving, premises contain and a conclusion also has to contain temporal conditions. A theorem prover must be able to utilize formal possibilities of Temporal logic. It must be able to manipulate them, produce legitimate transformation, substitute a temporal operator with another, transit from a state to another state.

With all of this overview in mind, it would be a conclusion. It is almost certain that a program is taken and modeled in Temporal logic.


Tags: ,

Comments are closed.