Declarative Programming with Temporal Constraints, in the Language CG
Specifying and reasoning about phenomena that evolve in
time are essential traits of any intelligent system. Their key components are
usually identified as (i) representing the temporal behaviour of a system and
(ii) extracting information which is otherwise implicit in the system
representation. In the traditional line of research, temporal representation
and reasoning are deployed for (program) verification .
Thus, the entire system behaviour is encoded by some form
of labelled transition graph (Kripke Structure), and temporal logic is used for
expressing specific properties of the underlying system.
Finally, model checking is employed for verifying whether
the property is entailed by the system at hand. Unlike the traditional
approach, we focus on capturing nonnecessarily deterministic evolutions of a
system. Thus, instead of characterizing all possible behaviours, by unfolding,
for example, a transition system and examining all paths, we look at a single
“evolution path.” We consider that our approach has interesting advantages with
respect to the traditional line of research based on temporal logics such as
LTL, CTL (for a more detailed motivation see, e.g., )
We are less interested in eventuality (e.g., fairness
constraints) or maintenance (e.g., safety constraints) of properties, which are
typical for model checking [4–7] and for deductive reasoning [8–11] in temporal
logics. Instead, we would like to identify temporal relations in the occurrence
of properties, in the spirit of Allen’s Interval Algebra [12]. As an example,
consider identifying “those individuals which were married at least twice.”
This amounts to finding those properties “married” which occur one after the
other and which enrol the same individual.
No comments:
Post a Comment