The need to extend traditional temporal logics to express and prove properties typical of stack-based formalisms led, among others, to CaRet and NWTL on Visibly Pushdown Languages (VPL). Such formalisms support, e.g., model checking of procedural programs and other context-free languages (CFL). To further and signi cantly extend their expressive power, we recently introduced the logic OPTL, based on Operator Precedence Languages (OPL) which cover a much wider subclass of CFL. In this communication we survey the latest developments of our work. We introduced a novel temporal logic, POTL, that rede nes OPTL to be First-Order complete. Furthermore, POTL's semantics is better connected to the typical treestructure of CFL while retaining the ability to reason about linear time. Besides the theoretical advancements, we are also moving steps toward the implementation of POTL model checking.
The need for specifying requirements in model checking with formalisms more
expressive than classical Linear Temporal Logic (LTL) has motivated much
research towards the development of formalisms capable of expressing context-free
properties [
Such logics, however, su er from the limited generality of VPL with respect to general CFL. This restricts the nesting relation on which they reason to be ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
call ret han exc call l =: l m hraent ml mm ml =m: exc m m m m #[call[[han[call[call[call]]]exc]call ret]ret]# Simple chains: call[call]exc, call[han exc]call Composed chains: call[call[call]]exc call[[han[call[call[call]]]exc]call ret]call ·
m # (0) · # (10) l . m call (1) = · ret (9) l l· call (7) =. remt (8)
. m han (2) = · exc (6) l call (3) · m m l call (4) · l call (5) one-to-one, which is enough for modeling the matching between function calls and returns in procedural programs. However, it is not adequate to represent more complex constructs such as exceptions and continuations, which need to be modeled by one-to-many or many-to-one relations. E.g., an exception is a single event that needs to be put in relation with all function instances it terminates.
To further expand the expressiveness of temporal logics we introduced OPTL
[
One of the features that is generally expected from temporal logics is
equivalence to FO Logic. Since proving this property for OPTL seems arduous, as is for
CaRet, in [
OPL have been inspired by precedence relations among operators in arithmetic expressions parsing. They are generated by grammars in operator form, i.e. whose rules' right-hand sides (rhs) have no consecutive non-terminals. Their parsers are guided in recognizing and reducing grammar rhs by three binary precedence relations (PR) among terminal symbols. Given two terminals a; b, for any non-terminals A; B; C and mixed terminal/non-terminal strings ; ; , we say a yields precedence to b (a l b) if there exists a rule A ! aC , s.t. a string Bb or b derives from C in any number of passes; a is equal in precedence to b (a =: b) if there exists a rule A ! aCb or A ! ab ; and a takes precedence over b (a m b) if there is a rule A ! Cb , s:.t. aB or a derives from C. In practice, a l b if b is the beginning of a rhs; a = b if they belong to the same rhs; a m b if a is the end of a rhs. If at most one PR holds between any terminal pair, once all PR are collected into an operator precedence matrix (OPM), the syntax tree (ST) of any word on the same alphabet is fully determined.
The way PR determine the ST of a string is formalized by chains: tDhaet:nci0t;ico`n+:112. A s[imfp#leg,chciai2n c0 [cf1ocr2e:v:e:rcy`]ci`+=1 1is; 2a; s:t:r:i`ng(`c0c11c)2,: a::ncd`cc`0+l1, cs1uc=:h c2 : : : c` 1 = c`mc`+1. A composed chain is a string c0s0c1s1c2 : : : c`s`c`+1, where c0 [c1c2 : : : c`]c`+1 is a simple chain, and si 2 is the empty string or is such that ci [si]ci+1 is a chain (simple or composed), for every i = 0; 1; : : : ; ` (` 1). Such a composed chain will be written as c0 [s0c1s1c2 : : : c`s`]c`+1 . c0 (resp. c`+1) is called its left (resp. right) context.
Fig. 1 shows OPM Mcall, together with word # call han call call call exc call ret ret #. Its chain structure is shown by surrounding chain bodies with brackets. The word is delimited by #, s.t. # l a and a m # for any terminal a. In the ST, each simple chain body corresponds to a rhs in the tree, and composed chains contain non-terminals, which are the bodies of other simple or composed chains. Thus, the structure of chains in a given string is isomorphic to its ST.
OPL also have a de ning class of pushdown automata, Operator Precedence
Automata [
Given a nite set of atomic propositions AP , the syntax of POTL follows: ' ::= a j :' j ' _ ' j #t' j t' j tF ' j tP ' j ' U t ' j ' St '
j #tH ' j tH ' j ' U Ht ' j ' SHt ' where a 2 AP , and t 2 fd; ug.
The semantics of POTL is based on the word structure {also called OP word for short{ hU; MP(AP ); P i, where U = f0; 1; : : : ; n; n + 1g, with n 2 N is a set of word positions; MP(AP ) is an OPM on P(AP ); P : U ! P(AP ) is a function associating each word position in U with the set of atomic propositions that hold in that position, with P (0) = P (n + 1) = f#g.
We use a partitioning of AP into a set of normal propositional labels (in round font), and structural labels (SL, in bold). SL de ne the OP structure of the word: MP(AP ) is only de ned for subsets of AP containing exactly one SL,
# l call l han l call l call l call m exc m call =: ret m ret m #
pA pB pC pC pErr pErr pA 0 1 2 3 4 5 6 7 8 9 10 so that given two SL l1; l2, for any a; a0; b; b0 2 P(AP ) s.t. l1 2 a; a0 and l2 2 b; b0 we have MP(AP )(a; b) = MP(AP )(a0; b0). This way, we de ne an OPM on P(AP ) by only giving relations between SL, as we did for Mcall. Given two positions i; j and a PR 2 fl; =: ; mg, we write i j to say P (i) P (j).
We de ne the chain relation U U so that (i; j) holds between two positions i; j i i < j 1, and i and j are resp. the left and right contexts of the same chain. For composed chains, may not be one-to-one, but also one-to-many or many-to-one. Fig. 2 shows the execution trace of a procedural program. The relation is meaningful w.r.t. the program semantics: every call to a function is in relation with the ret terminating it, and all instructions issued by that function are contained between them. calls terminated by an exception are in relation with the corresponding exc statement, so the chain relation is many-to-one.
The truth of POTL formulas is de ned w.r.t. a single word position. Let w be an OP word, and a 2 AP . Then, for any position i 2 U of w, we have (w; i) j= a if a 2 P (i). Operators such as ^ and : have the usual semantics from propositional logic. Next, while giving the formal semantics of POTL operators, we illustrate it by showing how it can be used to express properties on program execution traces, such as the one of Fig. 2.
Next/back operators. The downward next and back operators #d and d are like their LTL counterparts, except they are true only if the next (resp. current) position is at a lower or equal ST level than the current (resp. preceding) one. aiTnhd(ew(u;ipiw+a11r))d lj=nie'xotraan(ndidi lb1a)(cik=+:, 1i#.)uSourabnisd=t:it(uuit+,ea1lr)e, wsaynitmdh m(mwet;trioi)cj.o=bFtoardimn'atilhlye,(ws(ew;mi; ai)n1tj=)icj=s#fd'o'r, #u and u. E.g., #dcall means that the next position is an inner call (it holds in pos. 2, 3, 4 of Fig. 2), dcall to say that the previous position is a call, and the current is the rst of the body of a function (pos. 2, 4, 5), or the ret of an empty one (pos. 8).
The chain next and back operators tF and tP evaluate their argument respectively on future and past positions in the chain relation with the current one. The downward (resp. upward ) variant only considers chains whose right context goes down (resp. up) in the ST. (w; i) j= dF ' i there exists a position ja >poisistuiocnh tjh<ati s(uic;hj)t,hialtj o(rj;ii)=:, jj,lanidor( wj;=:j)i,j=an'd. ((ww;;ij))j=j= 'dP. 'Riepltahceerelexwiistths m for the upward versions. E.g., in pos. 1 of Fig. 2, dF pErr holds because (1; 7), meaning that pA calls pErr at least once. Also, uF exc is true in call positions whose procedure is terminated by an exception thrown by an inner procedure (e.g. pos. 3 and 4). uP call is true in exc statements that terminate at least one procedure other than the one raising it, such as the one in pos. 6. dF ret and uF ret hold in calls to non-empty procedures that terminate normally, and not due to an uncaught exception (e.g., pos. 1).
Until/Since operators. The summary until U t (resp. since St ) operator iIst ohbotldasiniendabpyosinitdiounctiifveeiltyhearpplhyoinldgs,thoer #thoalndds wtFith(r#estp(. Utt a)n(dresptP.)otp(eraSttor)s). or tF ( U t ) (resp. tP ( St )). It is an until on paths that move not only between consecutive positions, but also between contexts of a chain, skipping its body. With OPM Mcall, this means skipping function bodies. The downward variants move between positions at the same level in the ST (i.e., in the same simple chain body), or down in the nested chain structure. The upward ones move at the same or to higher levels of the ST. Formula > U u exc is true in positions contained in the frame of a function that is terminated by an exception. It is true in pos. 3 of Fig. 2 because of path 3-6, and false in pos. 1, because no path can enter chain (1; 9). Formula > U d exc is true in call positions whose function frame contains excs, but that are not directly terminated by one of them, such as the one in pos. 1 (with path 1-2-6). Moreover, call U d (ret ^ pErr ) holds in pos. 1 because of path 1-7-8, (call _ exc) Su pB in pos. 7 because of path 3-6-7, and (call _ exc) U u ret in 3 because of path 3-6-7-8.
Hierarchical Operators These operators enable reasoning on multiple positions in the chain relation with a single one. The upward and downward hierarchical next are de ned as (w; i) j= #uH ' i there exist a position h < i s.t. (h; i) and h l i and a position j = minfk j i < k ^ (h; k) ^ h l kg and (w; j) j= '; (w; i) j= #dH ' i there exist a position h > i s.t. (i; h) and i m h and a position j = minfk j i < k ^ (k; h) ^ k m hg and (w; j) j= '. Their past counterparts are symmetric, and their until and since operators are obtained by iterating them.
We proved the following claims on POTL's expressivity: Theorem 1. POTL = FO with one free variable on nite OP words. Corollary 1. NWTL
Moreover, we developed an automata-theoretic model checking procedure, whose complexity is not asymptotically greater than comparable formalisms: Theorem 2. Given a POTL formula ', it is possible to build an OPA A' accepting the language denoted by ' with at most 2O(j'j) states.
A' can then be intersected [
We surveyed our work on POTL, a novel temporal logic based on OPL, for which we proved FO-completeness. We gave a model-checking procedure based on automata construction, which we implemented in a prototype tool. We plan to further develop such tool to apply POTL to veri cation tasks.