Graded CTL* over finite paths

Abstract

In this paper we introduce Graded Computation Tree Logic over finite paths (GCTLf , for short), a variant of Computation Tree Logic CTL , in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTLf are interpreted over Kripke structures with a designated set of states, which we call "check points". These special states serve to delineate the end points of the finite executions. The syntax of GCTLf has path quantifiers of the form E g which express that there are at least g many distinct finite paths that a) end in a check point, and b) satisfy . After defining and justifying the logic GCTLf , we solve its model checking problem and establish that its computational complexity is PSPACE-complete.

Introduction

Temporal logics are a special kind of modal logics in which the truth values of the assertions vary with time [24]. Introduced in the seventies, these logics provide a very useful framework for checking the reliability of reactive systems, i.e., systems that continuously interact with the external environment. In formal verification [ 7,8,21,25 ] to check whether a system meets a desired behaviour, we check, by means of a suitable algorithm, whether a mathematical model of the system satisfies a formal specification of the required behaviour, the latter usually given in terms of a temporal-logic formula.

Depending on the view of the underlying nature of the time, we distinguish between two types of temporal logics. In linear-time temporal logics (such as LTL [24]) each moment in time follows a unique possible future. On the other hand, in branching-time temporal logics (such as CTL [ 7 ] and CTL? [ 13 ]) each moment in time can be split into various possible futures. In order to express properties along one or all the possible futures, branching logics make use of existential and universal path quantifiers.

Driven by the need to capture some specific system requirements, several variants and extensions of classic temporal logics have been considered over the years. One direction concerns the use of graded path modalities in branching-time temporal logics [ 3,18,26,14,6,1,17,20,2,22 ]. These modalities allow us to express properties such as "there exists at least n possible paths that satisfy a formula" or "all but n paths satisfy a formula". In [ 5 ], the authors introduce the extension of CTL with graded modalities, namely GCTL. They prove that, although GCTL is more expressive than CTL, the satisfiability problem for GCTL remains solvable in ExpTime, even in the case the graded numbers are coded in binary. In [ 16 ] the authors consider the model-checking problem using formulas expressed in GCTL and investigate its complexity: given a GCTL formula ' and a system model represented by a Kripke structure K, the model-checking problem can be solved in time (jKj j'j), that is the same running time required for CTL. In [ 2 ], the logic GCTL? was investigated. First, it was proved that it is equivalent, over trees, to Monadic Path Logic. Then, the authors turn to the satisfiability problem and show that it is 2ExpTime-complete. Finally, they show that the complexity of the model checking problem is PSpace-complete. So, for both decision problems we have the same complexity as for CTL?, although GCTL? is strictly more expressive.

Another meaningful direction concerning variations of classic temporal logics concerns the interpretation of formulas over finite paths [ 10,9,19,11,12 ]. The motivation for this is that many areas of Artificial Intelligence and Computer Science involve finite executions. A seminal work in this setting is [ 10 ], where the LTL logic framework was revisited under this assumption. In [ 10 ] it was proved that the resulting logic, namely LTLf , has the expressive power of First Order Logic. Also, it was proved that satisfiability and model-checking are PSpace-complete, thus not harder than LTL. Branching-time temporal logics interpreted over finite paths were also introduced and studied in the literature [ 27,13 ]. Very recently, this was also investigated for logics of strategic reasoning [ 4 ].

Although the interpretation of graded formulas over finite computations seems natural and useful in practice, surprisingly this specific combination has never been addressed in the literature. In formal verification, such a formalism could be useful to accelerate the process of finding bad computations (similarly to what was done in [ 15,16 ] for infinite computations) or to check an unambiguous satisfaction of a property (similarly to what was done in [ 1 ] for infinite computations).

Our Contribution. In this paper we introduce a variant of Computation Tree Logic (CTL ), namely GCTLf , in which path quantifiers E g are graded and interpreted over finite paths. The difference with CTL? is that we restrict the evaluation of formulas to finite paths and, that it makes use of a grade g (a natural number or infinity) that is coupled with the path quantifiers E and A in order to count paths. GCTLf formulas are interpreted over Kripke structures that are additionally annotated by marked states which we call check points. As the name advocates, these states represent moments along a system computation that should be inspected (by the formula). We address the computational complexity of the model-checking problem for GCTLf . The complexity is PSpace-hard, a fact that already holds for the fragment of formulas in which g = 1 [ 4 ]. On the other hand, we provide a matching upper-bound using a mix of automata-theory and nondeterministic algorithms.

Outline This paper is structured in the following way. In Section 2 we present some basic known concepts about automata and directed graphs that we use to solve our problem. In Section 3 we introduce and discuss the syntax and semantics of GCTLf . In Section 4 we provide a PSpace algorithm for the model checking problem of GCTLf . Finally, in Section 5 we give some possible future directions.

Preliminaries

In this section, we provide basic concepts about graphs and automata that we will use. As these are common definitions, an expert reader can skip this part. Directed Graphs A graph G is pair (V; E) where V is a finite set of vertices (also, called states nodes or points) and E V V is a set of edges (also, called arcs or lines). A path in G, of length m, is a sequence of m vertices v0; :::; vm 1 such that, for each i = 1; :::; m 1 we have that (vi 1; vi) 2 E. Given two vertices va and vb, we also say that vb is reachable from va if there exists a path of length at least 1 that starts with va and ends with vb. A path is called simple if no vertex appears more than once.

Nondeterministic Finite Word Automaton. A Nondeterministic Finite Word Automaton (NFW, for short) is a tuple A = (AP; N; I; ; F) where – AP is a finite non-empty set of atomic propositions ; – N is a finite non-empty set of states ; – I N is a non-empty set of initial states ; – : N 2AP ! 2N is a transition function; – F N is a set of final states.

Intuitively, (s; ) is the set of states that A can move into when it is in the state s and reads a subset of atoms 2 2AP. The automaton A is deterministic (DFW, for short) if jIj = 1 and j (s; )j = 1 for each state s and input 2 2AP.

A run r of A on a word w = 0; 1; :::; m 1 2 (2AP) is a sequence s0; s1; :::; sm of m + 1 states (i.e., elements of N ) such that s0 2 I and si+1 = (si; i) for 0 i < m. A run r is accepting if sm 2 F. A word w is accepted by A if A has an accepting run on w. The language of A is the set of words accepted by A.

The size of an NFW A, denoted jAj, is the cardinality of N. 3

Graded Computation Tree Logic over finite paths

In this section, we introduce Graded Computation Tree Logic over finite paths (GCTLf , for short), a variant of CTL in which the path quantifiers are graded and interpreted over finite paths. In particular, the syntax of GCTLf is an adaptation of branching-time logic with the following main features. On the one hand it restricts GCTL? [ 5 ] by considering finite paths that end in check points, and on the other hand it extends CTL? [ 13 ] by means of grades g 2 N [ f1g applied to the existential path quantifier E.

The obtained existential path operators E g expresses that there are at least g distinct paths satisfying . Just as for CTL?, the syntax includes path-formulas, expressing properties of paths, and state-formulas, expressing properties of states. Definition 1 (GCTLf syntax). GCTLf formulas are inductively built from a set of atomic propositions AP, by using the following grammar: := p j : j := j : j ^ ^ j E g

j E 1, j X j U where p 2 AP and g 2 N

All the formulas generated by a -rule are called state-formulas, while the formulas generated by a -rule are called path-formulas. The temporal operators are X (read "next") and U (read "until"). The path quantifier is E g (read "there exists at least g distinct paths..."). We introduce the following abbreviations: A<g = :E g: (read "all but less than g paths satisfy "), 1R 2 = :(: 1U: 2) (read "release"), F = trueU (read "eventually"), G = f alseR (read "globally"), and 1 _ 2 = :(: 1 ^ : 2) (read "or").

The semantics for GCTLf is defined w.r.t. a particular Kripke Structure in which there are special states which we call check points. It is a structure similar to a nondeterministic automaton and it is defined as follows.

Definition 2 (Kripke Structure System with check points). A Kripke Structure System with check points (KSc, for short) is a tuple K = hSt; AP; ; ; s0; Ci such that: – St is a finite non-empty set of states; – AP is a set of atomic propositions; – : St ! 2AP is the labeling function mapping each state to the atomic propositions true in that state; – St St is a transition relation; – s0 2 St is an initial state; – C St is a set of states called check points.

A path in K is a finite (resp., infinite) sequence of states 2 St (resp., St!) such that, for all i 2 [0; j j 1[ (resp., for all i 2 N) it holds that ( i; i+1) 2 . We define Pth(K) St! [ St to denote the sets of paths in K and we define Pth(s) to denote the set of paths starting from s. The first element of is denoted by fst( ) , 0, and its last by lst( ). Furthermore, we write ( )i , i to denote the i-th element of .

The semantics for GCTLf is defined w.r.t. KSc. The existential quantifiers E g express that there are at least g distinct paths ending in check points that satisfy . We distinguish finite paths 1, 2 2 Pth(K) of K in the natural way: two paths are distinct if they have different lengths, or if they have the same length, say m, and there exists an index 0 i < m such that that 1(i) 6= 2(i). Definition 3 (GCTLf Semantics). The semantics of GCTLf formulas is recursively defined for a KSc K, a state s, a path and a natural number i 2 N.

For state-formulas , 1, and 2: – K; s j= p if p 2 (s); – K; s j= : if K; s 6j= ; – K; s j= 1 ^ 2 if both K; s j= 1 and K; s j= 2; – K; s j= E g if there exists at least g distinct paths lst( ) 2 C and (b) K; ; 0 j= ; in Pth(s) such that (a) – K; s j= E 1 if there exists infinitely many distinct paths that (a) lst( ) 2 C and (b) K; ; 0 j= ; For path-formulas , , 1, and

2: – K; ; i j= if K; ( )i j= ; – K; ; i j= : if K; ; i 6j= ; – K; ; i j= 1 ^ 2 if both K; ; i j= 1 and K; ; i j= 2; – K; ; i j= X if i + 1 < j j and K; ; i + 1 j= ; – K; ; i j= 1U 2 if there exists k 2 N such that K; ; i + k j= j j= 1, for all j 2 [0; k[; 2 and K; ; i +

We say that satisfies the path formula over K, and write K; j= , if K; ; 0 j= . Also, we say that K satisfies the state formula , and write K j= , if K; s0 j= . We call a path formula without a path quantifier a flat path formula.

Note that a finite path satisfies X i is not the last position in . at position i implies, in particular, that Remark 1. The logic CTLf introduced in [ 4 ] is similar to GCTLf except that it does not have graded quantifiers, only E. That logic is a fragment of ours. To see this, simply restrict our logic to formulas in which every degree g is equal to 1. 4

Model Checking

In this section, we solve the model checking GCTLf and we provide an upper bound on its computational complexity. First, we define the decision problem. Definition 4. The model-checking problem for GCTLf is the following: given a KSc K and a GCTLf formula decide if K j= .

In order to measure the complexity, we need to define the size of the input K and . The size of a structure K is its number of states, and the size of a formula is defined as usual, except that jE g j = 1 + jgj + j j for g 6= 1, and jE 1 j = 1 + j j, i.e., the grades are represented in unary.

The main result of this section is that model checking GCTLf is in PSpace. Since model-checking CTLf is PSpace-hard [ 4 ], we get that model-checking GCTLf is PSpace-complete.

Theorem 1. The Model Checking Problem of GCTLf is in PSpace.

To prove this, we first provide an algorithm (Algorithm 1) that processes the state sub-formulas ' of , starting from the innermost one and, for each state s decides if (K; s) j= ' holds. The algorithm uses the following notions. A formula ' is a maximal state-subformula of if ' is a state-subformula of and ' is not a proper sub-formula of any other state sub-formula of . Every flat path formula of GCTLf formula can be viewed as an LTL formula whose atoms Algorithm 1 ModelChecking are elements of a maximal state-subformula logics, e.g., see [ 21 ]. as is usual for branching-time

Looking at Algorithm 1, we see that atomic case and the Boolean operations are immediate. For the path quantifier E g the algorithm relabels each state by a fresh atom p' iff the maximal state sub-formula ' of holds in that state. This is done recursively. It then treats as flat path formula by replacing each ' by p'. In Line 18, it converts into an NFW accepting all strings (over the alphabet 2AP) that satisfy the formula . This can be done using an adaptation of the classic Vardi-Wolper construction ([28]) for finite words [ 10 ]. In the last step, thanks to the algorithm ExistsP aths (Algorithm 2) we verify (in NLogSpace in jKj and jN j and PSpace in g) if there exist at least g distinct paths in K, each of which starts with s and ends with some vertex in C, each one labeling a word accepted by N . Note that the NFW may be of exponential size, but it can be built on-the-fly, i.e., there is a PSpace algorithm that computes the transition function of N (which is needed in Line 8 of Algorithm 2).

We now describe the Algorithm 2 for counting paths. The algorithm uses the following terminology: for a vertex v we let Adj(v) denote the set of vertices v0 such that (v; v0) 2 E. The idea of the algorithm is to guess g many different paths in K. It does this step-by-step, only storing the last state of each path. Note that to ease readability of the algorithm, there are implicit loops over the indices i; j g, e.g., in line 2, we set Kcuri to be s for every i.

Algorithm 2 ExistsPaths Proposition 1 (Counting Paths). The Algorithm ExistsP aths(K; s; N ; g) decides if there exist at least g distinct paths in K, each of which starts with s and ends with some vertex in C, each one labeling a word accepted by N . It works in NLogSpace in jKj and jN j, and PSpace in g.

Proof. The variables Kcuri are used in order to store the last state in K; they are initialised to s in line 2, and each path is advanced by one state in line 20 (i.e., if the path is not ended). The algorithm simultaneously also guesses g runs in N , one for each of the guessed paths in K. The variable Ncuri are used to store the last state of the ith guessed path in N ; it is initialised in line 3 by non-deterministically assigning it an element of the set I of initial states, and it is updated in line 8. In line 10, the algorithm also guesses when a given path in K finishes, and remembers this fact by setting the flag endedi to true. These flags initially are set to false in order to indicate that the ith path has not ended. The algorithm updates the variable Kdiffi;j , initially set to false (indicating that the two paths are not different) when it sees that the ith and jth path are different. This happens in one of two cases: (1) in some step, the ith path ended and the jth path did not (line 13), or (2) in some step, the current state of the ith path and jth path are different (line 22). Thus, if the algorithm returns YES (line 17) then there are g distinct paths in K, that (by guard 10) each end in C and label words accepted by N . On the other hand, suppose there exists g different sequences in K, each ending in C, and g corresponding sequences in N whose states are labeled by a word accepted by the automaton. Then we can use these paths to resolve the nondeterminism in lines 3, 8, 11 and 20, so that the algorithm returns YES.

Regarding the space complexity, first note that the algorithm is nondeterministic. Now, to store a vertex of a graph with N vertices we need logspace in N . The algorithm requires to store O(g) many such vertices. It also requires O(g2) many boolean variables (for the variables endedi and Kdif fi;j). tu 5

Conclusion and Future Work

Recently, temporal logic formalisms restricted to finite computations have received large attention in formal system verification. This concept is very important in many areas of Artificial Intelligence. For example, one may think of business processes that are modelled using finite path, or to automated planning in which the executions are often finite. In this paper we introduced a variant of CTL?, namely GCTLf , in which the formulas are interpreted over finite paths that can be selected by the logic by means of a graded modality. We addressed the model checking problem for GCTLf and proved it to be PSpace-complete.

Besides that, this articles opens several direction for future work. First, we recall that graded modalities have been studied also in the context of the modal -calculus, with and without backwards modalities [ 6 ]. It would be worth reconsidering that logic under the finite path semantics as we have done in this paper. Another interesting direction would be to consider enriching GCTLf with knowledge operators. Also, recent work shows how to count the number of strategies in a graph game [ 23,4 ], and extending our work to count strategies in the finite-trace case is of interest.

Finally, note that we have assumed in this paper that graded numbers used along formulas are coded in unary. By using a binary coding we immediately loose an exponent in the complexity of the model checking procedure. We leave open the question of whether this blow-up is avoidable (cf. [ 5 ]). 24. A. Pnueli. The Temporal Logic of Programs. In Foundation of Computer Science’77, pages 46–57. IEEE Computer Society, 1977. 25. J.P. Queille and J. Sifakis. Specification and Verification of Concurrent Programs in Cesar. In Symposium on Programming’81, LNCS 137, pages 337–351. Springer, 1981. 26. S. Tobies. PSPACE Reasoning for Graded Modal Logics. Journal of Logic and

Computation, 11(1):85–106, 2001. 27. M. Y. Vardi and L. Stockmeyer. Lower bound in full (2EXPTIME-hardness for

CTL-SAT). 1985. 28. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1–37, 1994.

References

1. Benjamin Aminof , Vadim Malvone, Aniello Murano, and Sasha Rubin . Graded modalities in strategy logic . Information and Computation , 261 : 634 - 649 , 2018 .

2. Benjamin Aminof , Aniello Murano, and Sasha Rubin . CTL* with graded path modalities . Information and Computation , 262 (Part 2): 1 - 21 , 2018 .

3. Everardo Bárcenas , Edgard Benítez-Guerrero, and Jesús Lavalle . On the model checking of the graded -calculus on trees . In MICAI 2015 , volume 9413 of Lecture Notes in Computer Science, pages 178 - 189 . Springer, 2015 .

4. Francesco Belardinelli , Alessio Lomuscio, Aniello Murano, and Sasha Rubin . Alternating-time temporal logic on finite traces . In International Joint Conference on Artificial Intelligence , pages 77 - 83 , 2018 .

5. A. Bianco , F. Mogavero , and A. Murano . Graded Computation Tree Logic. Transactions On Computational Logic , 13 ( 3 ): 25 : 1 - 53 , 2012 .

6. P.A. Bonatti , C. Lutz , A. Murano , and M.Y. Vardi . The Complexity of Enriched muCalculi. Logical Methods in Computer Science , 4 ( 3 ): 1 - 27 , 2008 .

7. E.M. Clarke and E.A. Emerson . Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic . In Logic of Programs'81, LNCS 131 , pages 52 - 71 . Springer, 1981 .

8. E.M. Clarke , O. Grumberg , and D.A. Peled . Model Checking. MIT Press, 2002 .

9. Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali . Reasoning on LTL on finite traces: Insensitivity to infiniteness . In AAAI , pages 1027 - 1033 , 2014 .

10. Giuseppe De Giacomo and Moshe Y. Vardi . Linear temporal logic and linear dynamic logic on finite traces . In IJCAI 2013 , pages 854 - 860 . IJCAI/AAAI, 2013 .

11. Giuseppe De Giacomo and Moshe Y. Vardi . Synthesis for LTL and LDL on finite traces . In Qiang Yang and Michael Wooldridge , editors, IJCAI 2015 , pages 1558 - 1564 . AAAI Press, 2015 .

12. Giuseppe De Giacomo and Moshe Y. Vardi. LTLf and LDLf synthesis under partial observability . In Subbarao Kambhampati, editor, IJCAI 2016 , pages 1044 - 1050 . IJCAI/AAAI Press, 2016 .

13. E.A. Emerson and J.Y. Halpern . “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time . Journal of the ACM , 33 ( 1 ): 151 - 178 , 1986 .

14. A. Ferrante , A. Murano , and M. Parente. Enriched Mu-Calculi Module Checking. Logical Methods in Computer Science , 4 ( 3 ): 1 - 21 , 2008 .

15. A. Ferrante , M. Napoli , and M. Parente . Graded-ctl: Satisfiability and symbolic model checking . In ICFEM 2009, volume LNCS 5885 , pages 306 - 325 , 2009 .

16. A. Ferrante , M. Napoli , and M. Parente . Model Checking for Graded CTL . Fundamenta Informaticae , 96 ( 3 ): 323 - 339 , 2009 .

17. M. Kaminski , S. Schneider , and G. Smolka . Terminating tableaux for graded hybrid logic with global modalities and role hierarchies . LMCS , 7 ( 1 ), 2011 .

18. Yevgeny Kazakov and Ian Pratt-Hartmann . A note on the complexity of the satisfiability problem for graded modal logics . In Symposium on Logic in Computer Science , pages 407 - 416 , 2009 .

19. Jeremy Kong and Alessio Lomuscio . Model checking multi-agent systems against LDLK specifications on finite traces . In AAMAS 2018 , pages 166 - 174 . IFAAMAS/ACM, 2018 .

20. O. Kupferman , U. Sattler , and M.Y. Vardi . The Complexity of the Graded muCalculus . In Conference on Automated Deduction'02, LNCS 2392 , pages 423 - 437 . Springer, 2002 .

21. O. Kupferman , M.Y. Vardi , and P. Wolper . An Automata Theoretic Approach to Branching-Time Model Checking . Journal of the ACM , 47 ( 2 ): 312 - 360 , 2000 .

22. Vadim Malvone , Fabio Mogavero, Aniello Murano, and Loredana Sorrentino . Reasoning about graded strategy quantifiers . Information and Computation , 259 : 390 - 411 , 2018 .

23. Vadim Malvone , Aniello Murano, and Loredana Sorrentino . Additional winning strategies in reachability games . Fundam . Inform., 159 ( 1-2 ): 175 - 195 , 2018 .