Temporal logic CTL \(+\) Prolog (Q1823654)

Let T denote closure of the set of formulas of the form P \((term_ 1,...,term_ n)\) under operation of conjunction and temporal operators of some kind (f. E. operators ``always'', ``until'' and so on), and TR be the set of formulas (rules) of the form \(f_ 1 \&...\& f_ m\to f_{m+1}\), where \(f_ i\) belongs to T. Let K be a (finite) Kripke structure, and L be an assignment of (finite) subsets of \(T\cup TR\) to worlds of K. A question \(?\)-P(t\({}_ 1,...,t_ m)\) with respect to a pair \(<K,L>\) is proposed to consider as a generalized Prolog-like program. An operational semantic based on stack machines is described for such programs when temporal operators are defined by Büchi automata. An interpreter written in Prolog is given in appendix for another somewhat different language of temporal programs. A lot of slightly motivated notation and misprints make the paper somewhat difficult to understand.