The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable
Abstract
The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL.
Keywords and phrases:
Satisfiability, temporal logics, probabilistic CTLCategory:
Track B: Automata, Logic, Semantics, and Theory of ProgrammingCopyright and License:
![[Uncaptioned image]](x1.png)
2012 ACM Subject Classification:
Theory of computation Modal and temporal logicsFunding:
The presented work received funding from the European Union’s Horizon Europe program under the Grant Agreement No. 101087529.Editors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele PuppisSeries and Publisher:

1 Introduction
Algorithms for checking the satisfiability/validity of formulae in a given logic have received significant attention from the very beginning of computer science. The satisfiability/validity problems are closely related to each other because for most logics we have that is valid iff is not satisfiable. The decidability of the validity problem for first-order logic, also known as the Entscheidungsproblem, was posed by Hilbert and Ackermann in 1928 and aswered negatively by Church [9] and Turing [22] in 1936. Later, Trakhtenbrot [21] demonstrated that the finite satisfiability problem for first-order logic is also undecidable. Consequently, the finite validity problem is not even semi-decidable, and hence there is no sound and complete deductive system proving all finite valid first-order formulae. For propositional logic, the satisfiability and validity are the canonical NP and complete problems [10].
The satisfiability and validity problems have also been intensively studied for temporal logics such as LTL, CTL, CTL∗, or the modal -calculus, and their computational complexity has been fully classified (see, e.g., [11, 20]). Temporal logics are interpreted over transition systems, i.e., directed graphs where the vertices correspond to the states of an abstract non-deterministic program, and the edges model the atomic computational steps. Even for the most expressive logic of the modal -calculus [14], the satisfiability/validity problems are decidable and EXPTIME-complete, and every satisfiable formula has a model whose size is at most exponential in (this is known as “the small model property” [15]). Furthermore, there is a sound and complete deductive system for the modal -calculus [23].
Probabilistic temporal logics, such as PCTL or PCTL∗ [12] are interpreted over discrete-time Markov chains modelling probabilistic programs. Despite numerous research attempts resulting in partial positive results (see Related work), the decidability of the satisfiability/validity problems for PCTL has remained unresolved for more than 30 years. In this paper, we prove that both problems are highly undecidable (i.e., beyond the arithmetical hierarchy), even for a simple PCTL fragment where the path connectives are restricted to and . Consequently, there is no sound and complete deductive system for PCTL.
Related work.
Unlike non-probabilistic temporal logics, PCTL does not have the small model property. In fact, one can easily construct satisfiable PCTL formulae without any finite model (see, e.g., [3]). Hence, the PCTL satisfiability/validity problems have also been studied in their finitary variants.
The first positive decidability results have been obtained for the qualitative fragment of PCTL, where the range of admissible probability constraints is restricted to , , , and (see Section 2 for details). The satisfiability/validity for qualitative PCTL is EXPTIME-complete, and the same holds for finite satisfiability/validity [18, 13, 16]. Furhermore, a finite description of a model for a satisfiable qualitative PCTL formula is constructible in exponential time [3]. The underlying proof techniques are similar to the ones used for non-probabilistic temporal logics.
The finite satisfiability is decidable also for certain quantitative PCTL fragments with general probability constrains [17, 5, 7]. The underlying arguments are mostly based on establishing an upper bound on the size of a model for a satisfiable formula of the considered fragment (the existence of a model can then be expressed in the existential fragment of first-order theory of the reals, which is known to be in PSPACE [4]). More concretely, in [5] it is shown that every formula of the bounded fragment of PCTL, where the validity of in a state depends only on a bounded prefix of a run initiated in , has a bounded-size tree model. In [17], several PCTL fragments based on and operators are studied. For each of these fragments, it is shown that every finite satisfiable formula has a bounded-size model where every non-bottom SCC is a singleton. For some of these fragments, it is shown that every satisfiable formula has a finite model, which yields the decidability of the (general) satisfiability problem. In [7], more abstract decidability results about finite PCTL satisfiability based on isolating the progress achieved along a chain of visited SCCs are presented. A variant of the bounded satisfiability problem, where transition probabilities are restricted to , is proven NP-complete in [1]. A recent result of [6] says that the finite satisfiability problem for unrestricted PCTL is undecidable. For a given Minsky machine, a PCTL formula is constructed so that every reachable configuration of the machine corresponds to a special state of a model. Hence, is always satisfiable, and has a finite model iff the set of reachable configurations of the machine is finite. Hence, the construction does not imply the undecidability of general PCTL satisfiability, and some of the crucial tools used in [6] apply only to finite Markov chains (see Section 4 for more comments).
Our contribution.
We show that the satisfiability problem for PCTL is hard for the level of the analytical hierarchy. Consequently, the PCTL validity problem is -hard. These results hold even for the PCTL fragment where only the path connectives are allowed. The proof is based on encoding the existence of a recurrent computation of a given non-deterministic two-counter machine by an effectively constructible PCTL formula . The overall structure of and the main underlying concepts are introduced in Section 3. In particular, in Section 3.2, we identify a fundamental obstacle that needs to be overcome when constructing . This is achieved by utilizing some concepts of convex geometry, and the solution is presented in Section 4. The construction of is then described in more detail in Section 5. Interestingly, our results imply that the finite satisfiability of the -fragment is also undecidable. This is a non-trivial refinement of the result achieved in [6], where the finite satisfiability is shown undecidable for PCTL formulae containing the , , , and path connectives.
The main technical contributions are the following. Non-negative integer counter values are represented by pairs of probabilities. More concretely, we fix a suitable representing zero, and then design a suitable function such that every is represented by the pair , where denotes the -fold composion of . The function is a modification of the function designed in [6]. Then, we prove that every (possibly infinite) satisfying a certain closure property must be contained in the convex polytope determined by the set of points (see Theorem 5). This is the crucial (novel) ingredient for overcoming the obstacles identified in Section 3.2. The second major technical contribution is a (novel) technique for representing the points by pairs of PCTL formulae of the -fragment.
The presented construction is non-trivial and technically demanding. We believe that, at least to some extent, this is caused by the inherent difficulty of the considered problem. We did our best to provide a readable sketch of the main steps in Section 5, where we also explain the purpose and use of Theorem 5. Full technical details are in [8].
2 Preliminaries
The sets of non-negative integers, rational numbers, and real numbers are denoted by , , and , respectively. We use to denote the elements of . The first and the second components of are denoted by and . For a function , we use to denote the -fold composition .
2.1 The Logic PCTL
The logic PCTL [12] is obtained from the standard CTL (Computational Tree Logic [11]) by replacing the existential and universal path quantifiers with the probabilistic operator . PCTL formulae are interpreted over Markov chains where every state is assigned a subset of propositions valid in .
Definition 1 (PCTL).
Let AP be a set of atomic propositions. The syntax of PCTL state and path formulae is defined by the following abstract syntax equations:
Here, , , is a rational constant, and .
A Markov chain is a triple , where is a finite or countably infinite set of states, is a probability matrix, and is a valuation. For , we say that is an immediate successor of if . A path in is a finite sequence of states where and for all . We say that is reachable from if there is a path from to . A run in is an infinite sequence of states such that every finite prefix of is a path in . We also use to denote the state of .
For every path , let be the set of all runs starting with , and let . To every state , we associate the probability space , where is the -field generated by all where starts in , and is the unique probability measure obtained by extending in the standard way (see, e.g., [2]). The validity of a PCTL state/path formula for a given state/run of is defined inductively as follows:
We say that is a model of if for some state of . The PCTL satisfiability problem is the question of whether a given PCTL formula has a model.
The formulae and the other Boolean connectives are defined using and in the standard way. In the following, we abbreviate a formula of the form by omitting and adjoining the probability constraint directly to the topmost path operator of . For example, we write instead of . We also use and to abbreviate the formulae and , respectively. Furthermore, abbreviates . Hence, iff .
2.2 Non-Deterministic -Counter Machines
Our results are obtained by constructing a PCTL formula encoding the existence of a recurrent computation in a given non-deterministic two-counter machine. However, the standard Minsky machines [19] are not particularly convenient for this purpose. More concretely, since every instruction modifies only one of the counters, a faithful simulation requires a mechanism for “copying” the other counter value to the next configuration. In other words, we need to implement not only the test-for-zero, increment, and decrement instructions, but also the “no-change” operation.
To avoid the need for implementing the “no-change” operation, we introduce a special variant of non-deterministic counter machines where every instruction performs an operation on all counters simultaneously. Let . A non-deterministic -counter machine is a finite sequence of instructions operating over non-negative counters , where every takes the form
(1) |
where , are non-empty subsets of target instruction indexes, and are counter updates. is deterministic if and are singletons in all . We use , , , and to denote the respective elements of .
The instruction (1) is executed as follows. First, the counter is tested for zero, and a successor label is chosen non-deterministically from either or , depending on whether the test succeeds or not, respectively. Then, simultaneously update the current values of . Here, inc increments the counter by one, and dec either decrements the counter by one or leaves the counter unchanged, depending on whether its current value is positive or zero, respectively. After that, the computation continues with . Note that the zero test is used only to determine the next instruction label.
More precisely, a configuration of is a tuple of the form where is the current instruction index, and are the current values of . A configuration is a successor of , written , if the following conditions are satisfied, where .
-
If then ; otherwise .
-
For all we have that is equal to either or , depending on whether is inc or dec, respectively.
A computation of is an infinite sequence of configurations such that and for all . A computation is bounded if it contains only finitely many pairwise different configurations, and -recurrent, where , if it contains infinitely many configurations of the form where .
In the next proposition, and denote the corresponding levels in the arithmetical and the analytical hierarchies, respectively. A proof is obtained by simulating the standard Minsky machines, see [8].
Proposition 2.
The problem of whether a given non-deterministic two-counter machine has a -recurrent computation (for a given ) is -hard. Furthermore, the problem of whether a given deterministic two-counter machine has a bounded computation is -hard.
3 Simulating Non-Deterministic Two-Counter Machines by PCTL
In this section, we give a high-level description of our undecidability proof, together with some preliminary intuition about the underlying techniques. The presented ideas are elaborated in subsequent sections.
Let be a non-deterministic two-counter machine with instructions. Our aim is to construct a PCTL formula such that
-
every model of contains a run representing a recurrent computation of ;
-
for every recurrent computation of there exists a model of representing the computation.
This entails the hardness of PCTL satisfiability.
In the following sections, we indicate how to construct for a given non-deterministic one-counter machine . The restriction to one counter leads to simpler notation without omitting any crucial ideas. The extension to non-deterministic two-counter machines is relatively simple (see Section 6). For the rest of this section, we fix a non-deterministic one-counter machine with instructions.
3.1 Representing the configurations of
The first step towards constructing the formula is finding a way of representing configurations of by “PCTL-friendly” properties of states in Markov chains.
More concretely, a state representing a configuration must encode the index and the non-negative integer . The is encoded by a dedicated atomic proposition valid in (for technical reasons, is actually a disjunction of several propositions). The way of encoding is more elaborate. Intuitively, the only unbounded information associated to that is “visible” to PCTL is the probability of satisfying certain path formulae in . The value of is encoded by a pair of probabilities of satisfying suitable path formulae and in . As we shall see, the formulae and depend on the state , but the only information about used to determine and is the (in)validity of certain atomic propositions in . Consequently, there are only finitely many PCTL formulae used to encode the counter values. The reason why cannot be represented just by a single probability of satisfying some appropriate path formula is indicated in Section 3.2.
It remains to explain which pair of probabilities encodes a given integer. Zero is encoded by a fixed (suitably chosen) pair , and if is encoded by , then is encoded by , where is a suitable function defined in Section 4.
To sum up, a state encodes a configuration iff and (recall that denotes the -fold composition of ).
3.2 Simulating a computational step of
The crucial part of our construction is the simulation of one computational step of . Let where . We show that for every , there exists a formula satisfying the following property:
Property 1.
For every computational step of the form and every state representing we have the following: If then
-
(i)
there exist and such that represents the configuration ;
-
(ii)
for every and every such that represents a configuration of , there exists such that represents the configuration .
The construction of is perhaps the most tricky part of our proof. At first glance, the above features (i) and (ii) seem unachievable because of the following fundamental obstacle.
Suppose that represents and . For simplicity, let us assume that the underlying Markov chain of has been unfolded into an infinite tree. According to (i), there exist and such that represents the configuration . For brevity, let us denote the states and by and , respectively. Since represents , we have that (see Section 3.1). Due to Property 1, (i) and (ii) must hold in an arbitrary modification of such that still represents and satisfies in . Now consider a modification where the immediate successor of is replaced with so that
-
(a)
every satisfies the same set of atomic propositions as ,
-
(b)
,
-
(c)
for every path subformula of . Here, is the probability of all runs initiated in satisfying .
Since this modification does not change the value of for any path subformula of , we have that after the modification. Note that (c) implies . However, if we choose so that every is different from , we may spoil both (i) and (ii).
Since spoiling the envisioned functionality of is so simple, one is even tempted to conclude the non-existence of . Indeed, no suitable can exist without some extra restriction preventing the use of arbitrary satisfying (a)–(c). We implement such a restriction with the help of basic convex geometry. First, observe that the condition (c) implies that is a convex combination of . We design the function so that the probability pairs representing non-negative integers are vertices (i.e., faces of dimension ) of a certain convex polytope. Furthermore, we identify a certain closure property preventing the use of such that is outside the polytope. Thus, whenever encodes a non-negative integer and is a positive convex combination of , we can conclude that every is inside the polytope, and consequently every is equal to because is a vertex of the polytope. Note that this would not be achievable if was a one-dimensional vector, i.e., if the counter values were encoded by the probability of satisfying a single path formula.
3.3 Constructing the formula
The formula expressing the existence of a recurrent computation of looks as follows:
where
Rec | ||||
The subformula Struct enforces certain “structural properties” of the model. says that the state satisfying represents the initial configuration . The subformula says that if the counter currently holds zero/positive value, then holds for some index of or , respectively. Rec enforces the existence of a run representing a -recurrent computation of . See Section 5 for more details.
4 Representing Non-Negative Integers by Points in
In this section, we show how to represent a non-negative counter value by a pair of quantities, and we design functions modeling the increment and decrement operations on the counter. Our starting point are the results invented for finite Markov chains in [6]. Our functions and are modifications of the functions and of [6], and the set of points determined by has a similar structure as the set of points determined by (see Fig. 1 left). The crucial novel ingredient is Theorem 5, which is applicable to arbitrary Markov chains, including infinite-state ones.
As we already indicated in Section 3, we aim to define suitable and such that every is encoded by , where is the -fold composition of . The points , , should be vertices of a certain convex polytope, and both and its inverse should be “expressible in PCTL”. Rougly speaking, the second condition means that if we have a state representing a configuration , then there exists a PCTL formula enforcing the existence of a successor of encoding the values obtained from by performing the instructions and . After many unsuccessful trials, we have identified a function satisfying these requirements. We put
where is a fixed constant. In Section 5, we set to a specific value. All observations presented in this section are valid for an arbitrary .
At first glance, is not a good choice because it is not even a function . However, there exists a subinterval such that . Furthermore, let
The properties of and are summarized in Lemma 3.
The slope of a line in , denoted by , is defined in the standard way. For all where , we use to denote the slope of the line containing .
Lemma 3.
Let and . For every we have the following:
-
(a)
;
-
(b)
;
-
(c)
and ; if , then ;
-
(d)
let ; then ;
-
(e)
let where . Then ;
-
(f)
if belongs to the line segment between and , then belongs to the line segment between and ;
-
(g)
.
Observe that by choosing a sufficiently small , the extreme points of can be pushed to values arbitrarily close to and . Let us fix some . The structure of is shown in Fig. 1 (left), where the dotted lines illustrate the property of Lemma 3 (d). Furthermore, Fig. 1 (left) also shows the convex polytope whose boundaries are the vertical lines going through the points and , the horizontal line going through the point , and all line segments between the consecutive points and . Note that is indeed convex by Lemma 3. Furthermore, each is a vertex (i.e., a face of dimension ) of . In our proof of Theorem 5, we also need the following lemma:
Lemma 4.
Let and . For all and such that , there exists such that , , and belongs to the line segment between and .
The next theorem is a crucial tool enabling the construction of the formula (see Section 3.2).
Theorem 5.
Let and . Furthermore, let be a finite or countably infinite subset of such that for every , the pair is a convex combination of the elements of . Then .
Proof.
We start by introducing some notation. For every line such that , we use to denote the closed half-space in above . Furthermore, for every , we use to denote the line containing the points and . Note that for every .
Now let be a set satisfying the assumptions of our lemma, and let . Note that if , then there exists such that by Lemma 3 (g). Observe that if then , which is a contradiction. Hence, .
Our aim is to show that . Suppose the converse. Due to the above observation, there exists such that . Let be the least such that . For every , let be the line with the same slope as containing the point .
Suppose that there exists such that . Then
-
if , we have that , hence is not a convex combination of the elements of , and we have a contradiction;
-
if , we obtain , which contradicts the minimality of .
Now suppose . Let be the supremum of all such that . Clearly, . Let
Note is a convex set and . We show that there exists such that . By the assumptions of our lemma, is a convex combination of the elements of . Since and is a convex set, this is impossible, and we have the desired contradiction.
The existence of such that is proven as follows. By the definition of , there is an infinite sequence such that for all and the distance of from approaches as . This sequence must contain an infinite subsequence converging to some point .
Since is continuous, it suffices to show that for all . Let us fix some . It follows directly from the definition of that (see Fig. 1 right). Hence, we have that either or . Let us first consider the case when . By Lemma 4, there exists such that , , and belongs to the line segment between and . By Lemma 3 (f), the point then belongs to the line segment between and . However, this line segment is disjoint with because its slope is strictly less than the slope of (see Lemma 3). A similar argument applies in the case when (see Fig. 1 right).
Observe that if is a set satisfying the assumptions of Theorem 5, then for every we have that if for some probability distribution over , then for all such that (because and is a vertex of ). When constructing the formula (see Section 5), we ensure that for all , the set of all , where ranges over a set of “relevant” states, satisfies the conditions of Theorem 5. Thus, we overcome the obstacle mentioned in Section 3.1.
5 Constructing the Formula
In this section, we show how to construct the formula simulating a given non-deterministic one-counter machine with instructions. The extension to two-counter machines is relatively simple and it is presented in Section 6.
When explaining the meaning of the constructed subformulae of , we often refer to some unspecified model of . Without restrictions, we assume that all states of the considered model are reachable from a state satisfying . The structure of has already been presented in Section 3. Recall that
where
Rec | ||||
We show how to implement the subformulae of , where is the main challenge.
Recall that the constant of Section 4 can be arbitrarily small. For our purposes, we need to choose , , , and (which exists for technical reasons) so that the extreme points of are rational, , and . For example, we can put , , , and . Furthermore, let
be sets of atomic propositions. For every , we use to denote , and for all and , let
5.1 Defining the basic structure of a model
Intuitively, states satisfying are the states where simulates the instruction of . The role of the index in is auxiliary. For every , we put . As we shall see, a state satisfying satisfies .
The formula Struct defines the basic structure of a model of . We put
Struct |
where
where
Let and . We say that is an marker if whenever , then for every reachable from . Note that this property can be encoded by the PCTL formula . The formula Mark says that
-
the sets , , , , and are markers,
-
the sets , , , , , , , , and are markers.
Finally, . The purpose of Lambda is clarified when constructing the formula .
The meaning of Struct is illustrated in Fig. 2. The first subformula of guarantees that if , then for almost all there is such that
-
for every ;
-
satisfies either , or , or , or , or , or .
This is shown in Fig. 2, together with the properties of states satisfying and enforced by the other subformulae of . The markers are typeset in boldface, and the probabilities constituting and are also shown. The meaning of Lambda is apparent in Fig. 2 (middle).
The three graphs of Fig. 2 describe the structure of every model of . As we shall see, implies . Almost every run initiated in eventually visits a state satisfying one of the six formulae shown in Fig. 2 (top). For example, suppose that . Since is a marker, this proposition is valid in all successors of . Furthermore, , and the structure of states reachable from is described in Fig. 2 (middle), i.e., almost every run initiated in eventually visits a state satisfying one of the six formulae shown in Fig. 2 (middle). If satisfies one the first five formulae, the states reachable from are no longer interesting (all of them satisfy the associated marker). If , the structure of states reachable from is shown in Fig. 2 (bottom).
The most interesting runs initiated in a state such that are the runs visiting infinitely many states satisfying a formula of the form (in Fig. 2 (top), keep following the rightmost branch). These runs are responsible for modelling the computations of .
5.2 Encoding the counter value
Now we define the path formulae and encoding the current value of the counter (see Section 3.1). Let . A state is relevant if it satisfies some proposition of (note that according to Struct, every relevant state satisfies exactly one proposition of ). If , we put and . Similarly, if , we put and . Furthermore, denotes the vector such that and are the probabilities of satisfying and in , respectively. We define as the set of all where is a relevant state. We need to ensure that satisfies the conditions of Theorem 5. Let
Eligible | ||||
where is the lower extreme point of (recall that is chosen so that is rational). Hence, for every relevant state , we have that iff . The formula Eligible says that for every relevant , i.e., . The closure property of Theorem 5 is enforced by the formulae constructed in the next paragraph.
5.3 The subformula
We put
The subformula says that a state satisfying represents the initial configuration of . The subformulae Eligible and , together with constructed below, ensure that the set introduced in the previous section satisfies the assumptions of Theorem 5 (as we shall see in Section 5.4, Decrement is similar to the formula implementing the dec operation on a counter).
We put
Decrement |
where
To explain the meaning of Decrement, suppose that , where is a state reachable from a state satisfying (hence, ). Let be the set of all states such that and , where is the probability of all runs initiated in such that visits and all states preceding this visit satisfy (see Fig. 3). The formula Decrement ensures that if , then , where . Hence, the condition of Theorem 5 is satisfied for .
More specifically, the subformula “copies” into , i.e., ensures that . We claim that
-
is the probability of satisfying the path formula in ;
-
is the probability of satisfying the path formula in .
Both claims follow directly from the formula Struct. However, the equality is not directly expressible in PCTL. Instead, the formula requires that and , where is the probability of satisfying the formula in . Note that
-
is the probability of satisfying the formula in .
-
is the probability of satisfying the formula in .
The first conjunct of says that the probability of satisfying in is equal to . By inspecting the structure of states reachable from , we obtain that the above formula is satisfied with the probability . Hence, which implies . Since , we have that
The second conjunct of says that the probability of satisfying in is also equal to , i.e., it is the same as the probability of satisfying . From this we obtain that the following two probabilities are also equal:
-
The probability of all runs initiated in visiting a state satisfying so that all states in preceding this visit do not satisfy .
-
The probability of all runs initiated in visiting a state satisfying so that all states in preceding this visit do not satisfy .
The first probability is equal to , and the second probability is equal to . Hence, . Since (see above), we obtain
To sum up, is a convex combination of where .
5.4 The subformula
Recall that
where
The purpose of the subformula of is to ensure that the index is “propagated” to the states reachable from a state satisfying (recall that Struct ensures the propagation of some counter index which may be different from ).
To explain the meaning of and the formula constructed below, let us assume that where is a state reachable form a state satisfying (in particular, ). We distinguish two subcases.
updates the counter by dec.
In this case, is similar to Decrement. We define the set of all states such that and , where is the probability of all runs initiated in such that visits and all states preceding this visit satisfy .
The formula ensures that if , then is a positive convex combination of where . In addition, it ensures that if , then is a positive convex combination of where . We put where
(2) | |||||
(3) |
where
By using similar arguments as in Section 5.3, it is easy to verify that
-
if , then ;
-
if , then .
updates the counter by inc.
Let be the set consisting of all such that and , where is the probability of all runs initiated in such that visits and all states preceding this visit satisfy . Furthermore, let be the set consisting of all such that and , where is the probability of all runs initiated in such that visits and all states preceding this visit satisfy . The formula ensures the following:
-
is a positive convex combination of where .
-
If , then is a positive convex combination of where .
We put where is the following formula:
(4) | |||||
(5) | |||||
(6) | |||||
(7) | |||||
(8) | |||||
(9) |
The meaning of is illustrated in Fig. 4. Suppose . Every subformula of specifies the probability of visiting a state of a certain family by a run initiated in . In Fig. 4, these families are indicated by colored shapes (some states belong to multiple families).
5.5 Justifying the correctness of
We claim that is satisfiable iff has a recurrent computation, i.e.,
-
if , then there is a run initiated in representing a recurrent computation of (here we use the results of Section 4);
-
for every recurrent computation of , there is a model of containing a run representing the computation.
We do not give explicit proofs for these claims since they are simplified versions of the proofs of Propositions 6 and 7 formulated in Section 6.
6 Extension to Non-Deterministic Two-Counter Machines
Now we show how to adapt the construction of presented in Section 5 when is a non-deterministic two-counter machine with instructions.
Let be non-deterministic one-counter machines obtained from by changing every instruction of form
into
where for and for . Observe that and do not simulate in any reasonable sense.
Consider the formulae and constructed for and in the way described in the previous sections, where the underlying sets and of atomic propositions are disjoint. For every subformula Form constructed in the previous sections, we use and to denote the corresponding formulae of and , respectively.
Intuitively, the formula is “basically” the conjunction of and with some additional synchronization. First, for every , let be the formula defined as follows:
-
If the counter tested for zero in is , then .
-
If the counter tested for zero in is , then .
Recall that and contain the subformulae and corresponding to the subformula
defined in Section 5.4. Let and be the formulae obtained from and by replacing the two and with and , where
Intuitively, replacing with ensures that the counter tested for zero in is indeed the counter tested for zero in . The reason for adding the third conjunct in and is more subtle. Roughly speaking, we cannot prevent the situation when a state satisfies but not (or vice versa). In this case, it does not make sense to continue the simulation of . However, we still need to ensure that the assumptions of Theorem 5 are satisfied. Therefore, we start to decrement the counter (or ).
Observe that and may still “choose” a different target label when simulating . Furthermore, even if they choose the same target label, the simulation of the counter’s updates is performed completely independently. Hence, there is no guarantee that a state encoding a configuration of can reach a state encoding a successor configuration . This is enforced by the formula
Sync |
Technically, Sync says that whenever a state satisfying is visited, then has a successor satisfying for some . Due to the subformulae and , the state must be visited form via a path such that all states except for satisfy . Note that has a successor satisfying the marker . Hence, the probability of all runs initiated in satisfying the formula
is positive (we could use other markers instead of ).
We put
where
Recurrent |
The formula Recurrent enforces the existence of a run representing a -recurrent computation of .
We say that a run of a Markov chain represents a computation of if there is an infinite increasing sequence of indexes such that for every , the state represents the configuration , i.e., if , then , , and .
Proposition 6.
If , then there exists representing a recurrent computation of .
Proof.
Let and . For a given state and , we say that is -relevant if satisfies some proposition of . For a -relevant state , we define as the pair of probabilities of satisfying the path formulae and in , respectively (see Section 5).
Let us fix a state such that . We put
It follows directly form the construction of that satisfies the assumptions of Theorem 5.
Consider the sequence of states definite inductively as follows:
-
. Observe that encodes the initial configuration of .
-
Consider the state encoding a configuration such that . For all , let be the set of all states such that and , where is the probability of all runs initiated in such that visits and all states preceding this visit satisfy . It follows from the construction of that the vector representing the counter value obtained from by performing is a positive convex combination of a set of vectors , where for every . By applying the results of Section 4, we obtain that for every . Hence, we can choose as an (arbitrary) element of which must be non-empty due to Sync. Note that encodes a successor configuration of .
The above sequence is not unique, and the runs associated with different sequences may represent different computations of . At least one of these computations must be -recurrent; otherwise, we obtain a contradiction with .
Proposition 7.
For every recurrent computation of there exist a Markov chain , a state of , and such that and represents the computation.
7 The Undecidability Results
The high undecidability of PCTL satisfiability is an immediate consequence of Propositions 6 and 7. Note that the formula constructed in in Section 6 uses only the path connective and the connectives , definable from . Hence, the high undecidability of PCTL satisfiability holds even for the -fragment of PCTL. Observe that is actually used only in the subformulae and . In [8], it is shown that these formulae can be rewritten so that they use only the connectives and . Hence, the result holds even for the -fragment of PCTL. Furthermore, when we omit the subformula enforcing the existence of a run representing a recurrent computation and assume that is deterministic, then the resulting formula has a finite model iff has a bounded computation. This means that finite PCTL satisfiability is undecidable even for the -fragment of PCTL. Thus, we obtain our main result.
Theorem 8.
The satisfiability problem for the -fragment of PCTL is -hard, and the finite satisfiability problem for the -fragment of PCTL is -hard.
Consequently, the validity problem for the -fragment is -hard, and the finite validity problem for the -fragment is -hard. This implies that there is no complete deductive system proving all valid (or finitely valid) formulae of the -fragment.
8 Conclusions
We have shown that the PCTL satisfiability problem is highly undecidable even for the -fragment. An interesting direction for future research is to characterize the decidability border for PCTL satisfiability, i.e., to establish principle boundaries of automatic probabilistic program synthesis from PCTL specifications.
References
- [1] N. Bertrand, J. Fearnley, and S. Schewe. Bounded satisfiability for PCTL. In Proceedings of CSL 2012, volume 16 of Leibniz International Proceedings in Informatics, pages 92–106. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPICS.CSL.2012.92.
- [2] P. Billingsley. Probability and Measure. Wiley, 1995.
- [3] T. Brázdil, V. Forejt, J. Křetínský, and A. Kučera. The satisfiability problem for probabilistic CTL. In Proceedings of LICS 2008, pages 391–402. IEEE Computer Society Press, 2008.
- [4] J. Canny. Some algebraic and geometric computations in PSPACE. In Proceedings of STOC’88, pages 460–467. ACM Press, 1988.
- [5] S. Chakraborty and J.P. Katoen. On the satisfiability of some simple probabilistic logics. In Proceedings of LICS 2016, pages 56–65, 2016.
- [6] M. Chodil and A. Kučera. The finite satisfiability problem for PCTL is undecidable. In Proceedings of LICS 2024, pages Article No. 22, pages 1–14. ACM Press, 2024.
- [7] M. Chodil and A. Kučera. The satisfiability problem for a quantitative fragment of PCTL. Journal of Computer and System Sciences, 139:103478, 2024. doi:10.1016/J.JCSS.2023.103478.
- [8] M. Chodil and A. Kučera. The satisfiability and validity problems for probabilistic computational tree logic are highly undecidable. arXiv, 2504.19207 [cs.LO], 2025.
- [9] A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58:345–363, 1936.
- [10] S.A. Cook. The complexity of theorem-proving procedures. In Proceedings of STOC’71, pages 151–158. ACM Press, 1971.
- [11] E.A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, B:995–1072, 1991.
- [12] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512–535, 1994. doi:10.1007/BF01211866.
- [13] S. Hart and M. Sharir. Probabilistic temporal logic for finite and bounded models. In Proceedings of POPL’84, pages 1–13. ACM Press, 1984.
- [14] D. Kozen. Results on the propositional -calculus. Theoretical Computer Science, 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.
- [15] D. Kozen. A finite-model theorem for the propositional -calculus. Studia Logica, 47(3):233–241, 1988. doi:10.1007/BF00370554.
- [16] S. Kraus and D.J. Lehmann. Decision procedures for time and chance (extended abstract). In Proceedings of FOCS’83, pages 202–209. IEEE Computer Society Press, 1983.
- [17] J. Křetínský and A. Rotar. The satisfiability problem for unbounded fragments of probabilistic CTL. In Proceedings of CONCUR 2018, volume 118 of Leibniz International Proceedings in Informatics, pages 32:1–32:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPICS.CONCUR.2018.32.
- [18] D. Lehmann and S. Shelah. Reasoning with time and chance. Information and Control, 53:165–198, 1982. doi:10.1016/S0019-9958(82)91022-1.
- [19] M.L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.
- [20] C. Stirling. Modal and temporal logics. Handbook of Logic in Computer Science, 2:477–563, 1992.
- [21] B. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. Proceedings of the USSR Academy of Sciences, 70(4):569–572, 1950.
- [22] A.M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230–265, 1937. doi:10.1112/PLMS/S2-42.1.230.
- [23] I. Walukiewicz. On completeness of the -calculus. In Proceedings of LICS’93, pages 136–146. IEEE Computer Society Press, 1993.