Abstract 1 Introduction 2 Preliminaries 3 Simulating Non-Deterministic Two-Counter Machines by PCTL 4 Representing Non-Negative Integers by Points in (𝟎,𝟏)𝟐 5 Constructing the Formula 𝝋𝓜 6 Extension to Non-Deterministic Two-Counter Machines 7 The Undecidability Results 8 Conclusions References

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable

Miroslav Chodil ORCID Faculty of Informatics, Masaryk University, Brno, Czech Republic Antonín Kučera ORCID Faculty of Informatics, Masaryk University, Brno, Czech Republic
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 CTL
Category:
Track B: Automata, Logic, Semantics, and Theory of Programming
Copyright and License:
[Uncaptioned image] © Miroslav Chodil and Antonín Kučera; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation Modal and temporal logics
Related Version:
Full Version: http://arxiv.org/abs/2504.19207 [8]
Funding:
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 Puppis

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 =0, >0, =1, and <1 (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 s depends only on a bounded prefix of a run initiated in s, 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 {12,1}, 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 Σ11 level of the analytical hierarchy. Consequently, the PCTL validity problem is Π11-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 𝙵k 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 𝒛(0,1)2 representing zero, and then design a suitable function 𝐼𝑛𝑐:(0,1)2(0,1)2 such that every n0 is represented by the pair 𝐼𝑛𝑐n(𝒛), where 𝐼𝑛𝑐n denotes the n-fold composion of 𝐼𝑛𝑐. The function 𝐼𝑛𝑐 is a modification of the function σ designed in [6]. Then, we prove that every (possibly infinite) T(0,1)2 satisfying a certain closure property must be contained in the convex polytope determined by the set of points {𝐼𝑛𝑐n(𝒛)n0} (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 𝐼𝑛𝑐n(𝒛) 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 𝒖1 and 𝒖2. For a function f:AA, we use fn to denote the n-fold composition ff.

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 P(Φ)r. PCTL formulae are interpreted over Markov chains where every state s is assigned a subset v(s)AP of propositions valid in s.

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:

φ::=a¬φφ1φ2P(Φ)rΦ::=𝚇φφ1𝚄φ2φ1𝚄kφ2

Here, aAP, {,>,,<,=,}, r[0,1] is a rational constant, and k.

A Markov chain is a triple M=(S,𝑃𝑟𝑜𝑏,v), where S is a finite or countably infinite set of states, 𝑃𝑟𝑜𝑏:S×S[0,1] is a probability matrix, and v:S2AP is a valuation. For s,tS, we say that t is an immediate successor of s if 𝑃𝑟𝑜𝑏(s,t)>0. A path in M is a finite sequence w=s0,,sn of states where n0 and 𝑃𝑟𝑜𝑏(si,si+1)>0 for all i<n. We say that t is reachable from s if there is a path from s to t. A run in M is an infinite sequence π=s0,s1, of states such that every finite prefix of π is a path in M. We also use π(i) to denote the state si of π.

For every path w=s0,,sn, let Run(w) be the set of all runs starting with w, and let (Run(w))=i=0n1𝑃𝑟𝑜𝑏(si,si+1). To every state s, we associate the probability space (Run(s),s,s), where s is the σ-field generated by all Run(w) where w starts in s, and s 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 M is defined inductively as follows:

saiffav(s),s¬φiffs⊧̸φ,sφ1φ2iffsφ1 and sφ2,sP(Φ)riffs({πRun(s)πΦ})r,π𝚇φiffπ(1)φ for some i,πφ1𝚄φ2iffthere is j0 such that π(j)φ2 and π(i)φ1 for all 0i<j,πφ1𝚄kφ2iffthere is 0jk such that π(j)φ2 and π(i)φ1 for all 0i<j.

We say that M is a model of φ if sφ for some state s of M. The PCTL satisfiability problem is the question of whether a given PCTL formula has a model.

The formulae true,false and the other Boolean connectives are defined using ¬ and in the standard way. In the following, we abbreviate a formula of the form P(Φ)r by omitting P and adjoining the probability constraint directly to the topmost path operator of Φ. For example, we write 𝚇=1φ instead of P(𝚇φ)=1. We also use 𝙵rφ and 𝙵rkφ to abbreviate the formulae true𝚄rφ and true𝚄rkφ, respectively. Furthermore, 𝙶rφ abbreviates 𝙵⋈̸r¬φ. Hence, s𝙶rφ iff s({πRun(s)π(i)φ for all i0})r.

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 d1. A non-deterministic d-counter machine is a finite sequence 𝐼𝑛𝑠1,,𝐼𝑛𝑠m of instructions operating over non-negative counters C1,,Cd, where every 𝐼𝑛𝑠 takes the form

Ck=0?Z : P:update1,,updated (1)

where k{1,,d}, Z,P{1,,m} are non-empty subsets of target instruction indexes, and update1,,updated{dec,inc} are counter updates. is deterministic if Z and P are singletons in all 𝐼𝑛𝑠. We use Ck, Z, P, and update1,,updated to denote the respective elements of 𝐼𝑛𝑠.

The instruction (1) is executed as follows. First, the counter Ck is tested for zero, and a successor label is chosen non-deterministically from either Z or P, depending on whether the test succeeds or not, respectively. Then, update1,,updated simultaneously update the current values of C1,,Cd. 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 (,c1,,cd) where {1,,m} is the current instruction index, and c1,,cd are the current values of C1,,Cd. A configuration (,c1,,cd) is a successor of (,c1,,cd), written (,c1,,cd)(,c1,,cd), if the following conditions are satisfied, where 𝐼𝑛𝑠Ck=0?Z : P:update1,updated.

  • If ck=0 then Z; otherwise P.

  • For all j{1,,d} we have that cj is equal to either cj+1 or max{0,cj1}, depending on whether updatej is inc or dec, respectively.

A computation of is an infinite sequence conf0,conf1, of configurations such that conf0=(1,0,,0) and conficonfi+1 for all i. A computation is bounded if it contains only finitely many pairwise different configurations, and τ-recurrent, where τ{1,,m}, if it contains infinitely many configurations of the form (i,c1,,cd) where iτ.

In the next proposition, Σ10 and Σ11 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 Σ11-hard. Furthermore, the problem of whether a given deterministic two-counter machine has a bounded computation is Σ10-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 m 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 Σ11 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 m 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 s representing a configuration (,c) must encode the index and the non-negative integer c. The is encoded by a dedicated atomic proposition 𝑎𝑡 valid in s (for technical reasons, 𝑎𝑡 is actually a disjunction of several propositions). The way of encoding c is more elaborate. Intuitively, the only unbounded information associated to s that is “visible” to PCTL is the probability of satisfying certain path formulae in s. The value of c is encoded by a pair of probabilities 𝜸[s](0,1)2 of satisfying suitable path formulae Φs and Ψs in s. As we shall see, the formulae Φs and Ψs depend on the state s, but the only information about s used to determine Φs and Ψs is the (in)validity of certain atomic propositions in s. Consequently, there are only finitely many PCTL formulae used to encode the counter values. The reason why c 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 n is encoded by 𝒗, then n+1 is encoded by 𝐼𝑛𝑐(𝒗), where 𝐼𝑛𝑐:(0,1)2(0,1)2 is a suitable function defined in Section 4.

To sum up, a state s encodes a configuration (,c) iff s𝑎𝑡 and 𝜸[s]=𝐼𝑛𝑐c(𝒛) (recall that 𝐼𝑛𝑐c denotes the c-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 {1,,m} where 𝐼𝑛𝑠C=0?Z : P:update. We show that for every ZP, there exists a formula 𝑆𝑡𝑒𝑝, satisfying the following property:

Property 1.

For every computational step of the form (,c)(,c) and every state s representing (,c) we have the following: If s𝑆𝑡𝑒𝑝, then

  1. (i)

    there exist πRun(s) and j1 such that π(j) represents the configuration (,c);

  2. (ii)

    for every πRun(s) and every j1 such that π(j) represents a configuration of , there exists 1jj such that π(j) represents the configuration (,c).

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 s represents (,c) and s𝑆𝑡𝑒𝑝,. For simplicity, let us assume that the underlying Markov chain of s has been unfolded into an infinite tree. According to (i), there exist πRun(s) and j1 such that π(j) represents the configuration (,c). For brevity, let us denote the states π(j1) and π(j) by u and t, respectively. Since t represents (,c), we have that 𝜸[t]=𝐼𝑛𝑐c(𝒛) (see Section 3.1). Due to Property 1, (i) and (ii) must hold in an arbitrary modification of such that s still represents (,c) and satisfies 𝑆𝑡𝑒𝑝, in . Now consider a modification where the immediate successor t of u is replaced with t1,,tn so that

  1. (a)

    every ti satisfies the same set of atomic propositions as t,

  2. (b)

    𝑃𝑟𝑜𝑏(u,t)=i=1n𝑃𝑟𝑜𝑏(u,ti),

  3. (c)

    𝑃𝑟𝑜𝑏(u,t)(Φ,t)=i=1n𝑃𝑟𝑜𝑏(u,ti)(Φ,ti)    for every path subformula Φ of 𝑆𝑡𝑒𝑝,. Here, (Φ,q) is the probability of all runs initiated in q satisfying Φ.

Since this modification does not change the value of (Φ,s) for any path subformula Φ of 𝑆𝑡𝑒𝑝,, we have that s𝑆𝑡𝑒𝑝, after the modification. Note that (c) implies 𝑃𝑟𝑜𝑏(u,t)𝜸[t]=i=1n𝑃𝑟𝑜𝑏(u,ti)𝜸[ti]. However, if we choose t1,,tn so that every 𝜸[ti] is different from 𝜸[t], 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 t1,,tn satisfying (a)–(c). We implement such a restriction with the help of basic convex geometry. First, observe that the condition (c) implies that 𝜸[t] is a convex combination of 𝜸[t1],,𝜸[tn]. We design the function 𝐼𝑛𝑐 so that the probability pairs representing non-negative integers are vertices (i.e., faces of dimension 0) of a certain convex polytope. Furthermore, we identify a certain closure property preventing the use of ti such that 𝜸[ti] is outside the polytope. Thus, whenever 𝜸[t] encodes a non-negative integer and 𝜸[t] is a positive convex combination of 𝜸[t1],,𝜸[tn], we can conclude that every 𝜸[ti] is inside the polytope, and consequently every 𝜸[ti] is equal to 𝜸[t] because 𝜸[t] is a vertex of the polytope. Note that this would not be achievable if 𝜸[t] was a one-dimensional vector, i.e., if the counter values were encoded by the probability of satisfying a single path formula.

The details are given in Section 4. The design of 𝐼𝑛𝑐 is also influenced by the need of “implementing” 𝐼𝑛𝑐 and its inverse 𝐷𝑒𝑐 in PCTL. The implementation requires additional non-trivial tricks described in Section 5.

3.3 Constructing the formula 𝝋𝓜

The formula φ expressing the existence of a recurrent computation of looks as follows:

φStruct𝐼𝑛𝑖𝑡𝙶=1(=1m(𝑎𝑡𝑆𝑖𝑚))Rec

where

Rec 𝙶=1(=1m(𝑎𝑡𝙵>0(τ𝑎𝑡)))
𝑆𝑖𝑚 (𝑍𝑒𝑟𝑜Z𝑆𝑡𝑒𝑝,)(¬𝑍𝑒𝑟𝑜P𝑆𝑡𝑒𝑝,)

The subformula Struct enforces certain “structural properties” of the model. 𝐼𝑛𝑖𝑡 says that the state satisfying φ represents the initial configuration (1,0). The subformula 𝑆𝑖𝑚 says that if the counter C currently holds zero/positive value, then 𝑆𝑡𝑒𝑝, holds for some index of Z or P, 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 𝒛(0,1)2 and 𝐼𝑛𝑐:(0,1)2(0,1)2 such that every n is encoded by 𝐼𝑛𝑐n(𝒛), where 𝐼𝑛𝑐n is the n-fold composition of 𝐼𝑛𝑐. The points 𝒛, 𝐼𝑛𝑐(𝒛), 𝐼𝑛𝑐2(𝒛), 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 s representing a configuration (,c1,c2), then there exists a PCTL formula enforcing the existence of a successor of s encoding the values obtained from c1,c2 by performing the instructions update1 and update2. After many unsuccessful trials, we have identified a function satisfying these requirements. We put

𝐼𝑛𝑐(𝒗)=(λ1𝒗1,𝒗2λ1𝒗1)

where λ(0,14) is a fixed constant. In Section 5, we set λ to a specific value. All observations presented in this section are valid for an arbitrary λ(0,14).

At first glance, 𝐼𝑛𝑐 is not a good choice because it is not even a function (0,1)2(0,1)2. However, there exists a subinterval Iλ(0,1) such that 𝐼𝑛𝑐:Iλ×(0,1)Iλ×(0,1). Furthermore, let

𝐷𝑒𝑐(𝒗)=(𝒗1λ𝒗1,𝒗2𝒗1).

The properties of 𝐼𝑛𝑐 and 𝐷𝑒𝑐 are summarized in Lemma 3.

The slope of a line 𝐿𝑖𝑛𝑒 in 2, denoted by 𝑠𝑙𝑜𝑝𝑒(𝐿𝑖𝑛𝑒), is defined in the standard way. For all 𝒗,𝒖2 where 𝒗1𝒖1, we use 𝑠𝑙𝑜𝑝𝑒(𝒗,𝒖) to denote the slope of the line containing 𝒗,𝒖.

Lemma 3.

Let λ(0,14) and Iλ=(114λ2,1+14λ2). For every 𝐯Iλ×[0,1] we have the following:

  1. (a)

    𝐼𝑛𝑐(𝒗)Iλ×[0,1];

  2. (b)

    𝐷𝑒𝑐(𝐼𝑛𝑐(𝒗))=𝒗;

  3. (c)

    𝐼𝑛𝑐(𝒗)1<𝒗1 and 𝐼𝑛𝑐(𝒗)2𝒗2; if 𝒗2>0, then 𝐼𝑛𝑐(𝒗)2<𝒗2;

  4. (d)

    let 𝒖=(𝐼𝑛𝑐2(𝒗)1,0); then 𝑠𝑙𝑜𝑝𝑒(𝒖,𝐼𝑛𝑐(𝒗))=𝑠𝑙𝑜𝑝𝑒(𝐼𝑛𝑐(𝒗),𝒗);

  5. (e)

    let 𝒖=(𝐼𝑛𝑐(𝒗)1,y) where 0y<𝐼𝑛𝑐(𝒗)2. Then 𝑠𝑙𝑜𝑝𝑒(𝒖,𝐷𝑒𝑐(𝒖))<𝑠𝑙𝑜𝑝𝑒(𝐼𝑛𝑐(𝒗),𝒗);

  6. (f)

    if 𝒖 belongs to the line segment between 𝐼𝑛𝑐2(𝒗) and 𝐼𝑛𝑐(𝒗), then 𝐷𝑒𝑐(𝒖) belongs to the line segment between 𝐼𝑛𝑐(𝒗) and 𝒗;

  7. (g)

    limn𝐼𝑛𝑐n(𝒗)1=114λ2.

Observe that by choosing a sufficiently small λ>0, the extreme points of Iλ can be pushed to values arbitrarily close to 0 and 1. Let us fix some 𝒛Iλ×(0,1). The structure of 𝒛,𝐼𝑛𝑐(𝒛),𝐼𝑛𝑐2(𝒛), 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 (114λ2,0) and 𝒛, the horizontal line going through the point (0,1), and all line segments between the consecutive points 𝐼𝑛𝑐i(𝒛) and 𝐼𝑛𝑐i+1(𝒛). Note that 𝒜(𝒛) is indeed convex by Lemma 3. Furthermore, each 𝐼𝑛𝑐i(𝒛) is a vertex (i.e., a face of dimension 0) of 𝒜(𝒛). In our proof of Theorem 5, we also need the following lemma:

Lemma 4.

Let λ(0,14) and 𝐳Iλ×(0,1). For all 𝐯Iλ×[0,1]𝒜(𝐳) and n such that 𝐼𝑛𝑐n+1(𝐳)1𝐯1𝐼𝑛𝑐n(𝐳)1, there exists 𝐮 such that 𝐮1=𝐼𝑛𝑐n+1(𝐳)1, 0𝐮2<𝐼𝑛𝑐n+1(𝐳)2, and 𝐯 belongs to the line segment between 𝐮 and 𝐷𝑒𝑐(𝐮).

Figure 1: The structure of 𝒛,𝐼𝑛𝑐(𝒛),𝐼𝑛𝑐2(𝒛), and 𝒜(𝒛) (left); the construction proving 𝑂𝑢𝑡= (right).

The next theorem is a crucial tool enabling the construction of the formula 𝑆𝑡𝑒𝑝, (see Section 3.2).

Theorem 5.

Let λ(0,14) and 𝐳Iλ×(0,1). Furthermore, let T be a finite or countably infinite subset of (114λ2,𝐳1)×(0,1) such that for every 𝐯T𝒜(𝐳), the pair 𝐷𝑒𝑐(𝐯) is a convex combination of the elements of T. Then T𝒜(𝐳).

Proof.

We start by introducing some notation. For every line 𝐿𝑖𝑛𝑒 such that 𝑠𝑙𝑜𝑝𝑒(𝐿𝑖𝑛𝑒)(0,), we use H(𝐿𝑖𝑛𝑒) to denote the closed half-space in 2 above 𝐿𝑖𝑛𝑒. Furthermore, for every n, we use 𝐿𝑖𝑛𝑒n(𝒛) to denote the line containing the points 𝐼𝑛𝑐n(𝒛) and 𝐼𝑛𝑐n+1(𝒛). Note that 𝒜(𝒛)H(𝐿𝑖𝑛𝑒n(𝒛)) for every n.

Now let T be a set satisfying the assumptions of our lemma, and let 𝑂𝑢𝑡=T𝒜(𝒛). Note that if 𝒗𝑂𝑢𝑡, then there exists n such that 𝐼𝑛𝑐n+1(𝒛)1𝒗1𝐼𝑛𝑐n(𝒛)1 by Lemma 3 (g). Observe that if 𝒗H(𝐿𝑖𝑛𝑒n(𝒛)) then 𝒗𝒜(𝒛), which is a contradiction. Hence, 𝒗H(𝐿𝑖𝑛𝑒n(𝒛)).

Our aim is to show that 𝑂𝑢𝑡=. Suppose the converse. Due to the above observation, there exists n such that 𝑂𝑢𝑡H(𝐿𝑖𝑛𝑒n(𝒛)). Let ν be the least n such that 𝑂𝑢𝑡H(𝐿𝑖𝑛𝑒n(𝒛)). For every 0y𝐼𝑛𝑐ν+1(𝒛)2, let Ly be the line with the same slope as 𝐿𝑖𝑛𝑒ν(𝒛) containing the point (𝐼𝑛𝑐ν+1(𝒛)1,y).

Suppose that there exists 𝒗𝑂𝑢𝑡 such that 𝒗H(L0). Then

  • if ν=0, we have that 𝐷𝑒𝑐(𝒗)1>𝒛1, hence 𝐷𝑒𝑐(𝒗) is not a convex combination of the elements of T, and we have a contradiction;

  • if ν>0, we obtain 𝒗H(𝐿𝑖𝑛𝑒ν1(𝒛)), which contradicts the minimality of ν.

Now suppose 𝑂𝑢𝑡H(L0). Let μ be the supremum of all y𝐼𝑛𝑐ν+1(𝒛)2 such that 𝑂𝑢𝑡H(Ly). Clearly, 0μ<𝐼𝑛𝑐ν+1(𝒛)2. Let

𝒳=[114λ2,𝒛1]×[0,1]H(Lμ)n=0ν1H(𝐿𝑖𝑛𝑒n(𝒛))

Note 𝒳 is a convex set and T𝒳. We show that there exists 𝒗𝑂𝑢𝑡 such that 𝐷𝑒𝑐(𝒗)𝒳. By the assumptions of our lemma, 𝐷𝑒𝑐(𝒗) is a convex combination of the elements of T. Since T𝒳 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 𝒖1,𝒖2, such that 𝒖i𝑂𝑢𝑡 for all i1 and the distance of 𝒖i from Lμ approaches 0 as i. This sequence must contain an infinite subsequence converging to some point 𝜶Lμ𝒳.

Since 𝐷𝑒𝑐 is continuous, it suffices to show that 𝐷𝑒𝑐(𝜶)𝒳 for all 𝜶Lμ𝒳. Let us fix some 𝜶Lμ𝒳. It follows directly from the definition of Lμ that 𝐼𝑛𝑐ν+2(𝒛)1<𝜶1<𝐼𝑛𝑐ν(𝒛)1 (see Fig. 1 right). Hence, we have that either 𝐼𝑛𝑐ν+2(𝒛)1<𝜶1𝐼𝑛𝑐ν+1(𝒛)1 or 𝐼𝑛𝑐ν+1(𝒛)1<𝜶1<𝐼𝑛𝑐ν(𝒛)1. Let us first consider the case when 𝐼𝑛𝑐ν+2(𝒛)1<𝜶1𝐼𝑛𝑐ν+1(𝒛)1. By Lemma 4, there exists 𝒖 such that 𝒖1=𝐼𝑛𝑐ν+2(𝒛)1, 0𝒖2<𝐼𝑛𝑐ν+2(𝒛)2, and 𝜶 belongs to the line segment between 𝒖 and 𝐷𝑒𝑐(𝒖). By Lemma 3 (f), the point 𝐷𝑒𝑐(𝜶) then belongs to the line segment between 𝐷𝑒𝑐(𝒖) and 𝐷𝑒𝑐2(𝒖). However, this line segment is disjoint with 𝒳 because its slope is strictly less than the slope of Lμ (see Lemma 3). A similar argument applies in the case when 𝐼𝑛𝑐ν+1(𝒛)1<𝜶1<𝐼𝑛𝑐ν(𝒛)1 (see Fig. 1 right).

Observe that if T is a set satisfying the assumptions of Theorem 5, then for every n we have that if 𝐼𝑛𝑐n(𝒛)=𝒗Tκ(𝒗)𝒗 for some probability distribution κ over T, then 𝒗=𝐼𝑛𝑐n(𝒛) for all 𝒗T such that κ(𝒗)>0 (because T𝒜(𝒛) and 𝐼𝑛𝑐n(𝒛) is a vertex of 𝒜(𝒛)). When constructing the formula φ (see Section 5), we ensure that for all k{1,2}, the set of all 𝜸k[t], where t 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 m 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

φStruct𝐼𝑛𝑖𝑡𝙶=1(=1m(𝑎𝑡𝑆𝑖𝑚))Rec

where

Rec 𝙶=1(=1m(𝑎𝑡𝙵>0(τ𝑎𝑡)))
𝑆𝑖𝑚 (𝑍𝑒𝑟𝑜Z𝑆𝑡𝑒𝑝,)(¬𝑍𝑒𝑟𝑜P𝑆𝑡𝑒𝑝,)

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 λ, 𝒛1, 𝒛2, and δ (which exists for technical reasons) so that the extreme points of Iλ are rational, 𝒛2<𝒛1<δ, and 2λ+2δ+2𝒛1+2𝒛2<1. For example, we can put λ=14255, Iλ=(115,1415), 𝒛=(112,115), and δ=111. Furthermore, let

= {K}{Ai,Bi,Ci,Di,Ei,Ri0i2}
𝒜 = {ai,,a¯i,,bi,,ci,,di,,ri,0i2,1m}

be sets of atomic propositions. For every i{0,1,2}, we use S(i) to denote i+1 mod 3, and for all O𝒜 and LO, let LOpLppOL¬p.

5.1 Defining the basic structure of a model

Intuitively, states satisfying ri, are the states where φ simulates the instruction 𝐼𝑛𝑠 of . The role of the index i in ri, is auxiliary. For every 1m, we put 𝑎𝑡r0,𝒜r1,𝒜r2,𝒜. As we shall see, a state satisfying φ satisfies r0,1𝒜.

The formula Struct defines the basic structure of a model of φ. We put

Struct 𝑆𝑢𝑐𝑐MarkLambda

where

𝑆𝑢𝑐𝑐 =1mi=02𝙶=1(ri,𝒜=1mri,𝒜𝚄=1rsuci,,)
i=02𝙶=1((RiRi𝚄=1Rsuci)(Ri,KRi,K𝚄=1RKsuci))

where

rsuci,, rS(i),𝒜j=02(ai,,Rj𝒜a¯i,,Rj𝒜bi,,Rj𝒜ci,,Rj𝒜di,,Rj𝒜)
Rsuci AiBiCiDiEiRS(i),K
RKsuci Ai,KBi,KCi,KDi,KRS(i),K

Let O𝒜 and LO. We say that L is an O marker if whenever sLO, then sLO for every s reachable from s. Note that this property can be encoded by the PCTL formula LO𝙶=1LO. The formula Mark says that

  • the sets {ai,}, {a¯i,}, {bi,}, {ci,}, and {di,} are 𝒜 markers,

  • the sets {Ai}, {Ai,K}, {Bi}, {Bi,K}, {Ci}, {Ci,K}, {Di}, {Di,K}, and {Ei} are markers.

Finally, Lambdai=02(Ri𝙶=λ(RiEi). The purpose of Lambda is clarified when constructing the formula 𝑆𝑡𝑒𝑝,.

Figure 2: Illustrating the meaning of Struct.

The meaning of Struct is illustrated in Fig. 2. The first subformula of 𝑆𝑢𝑐𝑐 guarantees that if sri,𝒜, then for almost all πRun(s) there is n such that

  • π(n)ri,𝒜 for every 0n<n;

  • π(n) satisfies either j=02ai,,Rj𝒜, or j=02a¯i,,Rj𝒜, or j=02bi,,Rj𝒜, or j=02ci,,Rj𝒜, or j=02di,,Rj𝒜, or rS(i),𝒜.

This is shown in Fig. 2, together with the properties of states satisfying Ri and Ri,K enforced by the other subformulae of 𝑆𝑢𝑐𝑐. The markers are typeset in boldface, and the probabilities constituting 𝜸[s]1 and 𝜸[s]2 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, sφ implies sr0,1𝒜. Almost every run initiated in s eventually visits a state s satisfying one of the six formulae shown in Fig. 2 (top). For example, suppose that sbi,,Rj. Since bi, is a marker, this proposition is valid in all successors of s. Furthermore, sRj, and the structure of states reachable from s is described in Fig. 2 (middle), i.e., almost every run initiated in s eventually visits a state s′′ satisfying one of the six formulae shown in Fig. 2 (middle). If s′′ satisfies one the first five formulae, the states reachable from s′′ are no longer interesting (all of them satisfy the associated marker). If s′′RS(j),K, the structure of states reachable from s′′ is shown in Fig. 2 (bottom).

The most interesting runs initiated in a state s such that sφ are the runs visiting infinitely many states satisfying a formula of the form ri, (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 Φs and Ψs encoding the current value of the counter C (see Section 3.1). Let ={ri,,Ri0i2,1m}. A state is relevant if it satisfies some proposition of (note that according to Struct, every relevant state satisfies exactly one proposition of ). If sri,, we put Φs𝙶(ri,ai,a¯i,) and Ψs𝙶(ri,bi,). Similarly, if sRi, we put Φs𝙶(RiAi) and Ψs𝙶(RiBi). Furthermore, 𝜸[s][0,1]2 denotes the vector such that 𝜸[s]1 and 𝜸[s]2 are the probabilities of satisfying Φs and Ψs in s, respectively. We define T as the set of all 𝜸[s] where s is a relevant state. We need to ensure that T satisfies the conditions of Theorem 5. Let

𝑍𝑒𝑟𝑜 i=02=1m(ri,(𝙶=𝒛1(ri,ai,a¯i,)𝙶=𝒛2(ri,bi,)))
i=02(Ri(𝙶=𝒛1(RiAi)𝙶=𝒛2(RiBi)))
Eligible i=02=1m𝙶=1(ri,(𝙶𝒛1(ri,ai,a¯i,)𝙶β(ri,ai,a¯i,)))
i=02𝙶=1(Ri(𝙶𝒛1(RiAi)𝙶β(RiAi)))

where β is the lower extreme point of Iλ (recall that λ is chosen so that β is rational). Hence, for every relevant state s, we have that s𝑍𝑒𝑟𝑜 iff 𝜸[s]=𝒛. The formula Eligible says that 𝜸[s]1((114λ/2),𝒛1) for every relevant s, i.e., T((114λ)/2,𝒛1)×(0,1). The closure property of Theorem 5 is enforced by the formulae constructed in the next paragraph.

5.3 The subformula 𝑰𝒏𝒊𝒕

We put

𝐼𝑛𝑖𝑡 r0,1𝒜𝑍𝑒𝑟𝑜Eligible𝙶=1Decrement

The subformula r0,1𝒜𝑍𝑒𝑟𝑜 says that a state satisfying φ represents the initial configuration (1,0) of . The subformulae Eligible and 𝙶=1Decrement, together with 𝑆𝑡𝑒𝑝, constructed below, ensure that the set T 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 i=02(Ri¬𝑍𝑒𝑟𝑜)(Copyi𝑆𝑢𝑐𝑐i)

where

Copyi 𝙶=δ(RiAiCi)𝙵=δ(RS(i)Ci)
𝑆𝑢𝑐𝑐i 𝙵=λ(BS(i)CS(i)DS(i)RS2(i))𝙵=λ(BiCS(i)DS(i)RS2(i))

To explain the meaning of Decrement, suppose that sRiDecrement, where s is a state reachable from a state satisfying φ (hence, sStruct). Let U be the set of all states u such that uRS(i)K and pu>0, where pu is the probability of all runs w initiated in s such that w visits u and all states preceding this visit satisfy Ri (see Fig. 3). The formula Decrement ensures that if s¬𝑍𝑒𝑟𝑜, then 𝐷𝑒𝑐(𝜸[s])=uU(pu/P)𝜸[u], where P=uUpu. Hence, the condition of Theorem 5 is satisfied for 𝜸[s].

More specifically, the subformula Copyi “copies” 𝜸[s]1 into P, i.e., ensures that P=𝜸[s]1. We claim that

  • P is the probability of satisfying the path formula 𝙵RS(i) in s;

  • 𝜸[s]1 is the probability of satisfying the path formula 𝙶(RiAi) in s.

Both claims follow directly from the formula Struct. However, the equality P=𝜸[s]1 is not directly expressible in PCTL. Instead, the formula Copyi requires that 𝜸[s]1+κ=δ and P+κ=δ, where κ is the probability of satisfying the formula 𝙶(RiCi) in s. Note that

  • P+κ is the probability of satisfying the formula 𝙵(RS(i)Ci) in s.

  • 𝜸[s]1+κ is the probability of satisfying the formula 𝙶(RiAiCi) in s.

The first conjunct of 𝑆𝑢𝑐𝑐i says that the probability of satisfying 𝙵(BS(i)CS(i)DS(i)RS2(i)) in s is equal to λ. By inspecting the structure of states reachable from s, we obtain that the above formula is satisfied with the probability uUpu(1𝜸[u]1). Hence, uUpu(1𝜸[u]1)=λ which implies (Pλ)/P=uU(pu/P)𝜸[u]1. Since P=𝜸[s]1, we have that

𝐷𝑒𝑐(𝜸[s])1=(𝜸[s]1λ)/𝜸[s]1=uU(pu/P)𝜸[u]1.

The second conjunct of 𝑆𝑢𝑐𝑐i says that the probability of satisfying 𝙵(BiCS(i)DS(i)RS2(i)) in s is also equal to λ, i.e., it is the same as the probability of satisfying 𝙵(BS(i)CS(i)DS(i)RS2(i)). From this we obtain that the following two probabilities are also equal:

  • The probability of all runs π initiated in s visiting a state satisfying Bi so that all states in π preceding this visit do not satisfy RS2(i).

  • The probability of all runs π initiated in s visiting a state satisfying BS(i) so that all states in π preceding this visit do not satisfy RS2(i).

The first probability is equal to 𝜸[s]2, and the second probability is equal to uUpu𝜸[u]2. Hence, 𝜸[s]2=uUpu𝜸[u]2. Since P=𝜸[s]1 (see above), we obtain

𝐷𝑒𝑐(𝜸[s])2=𝜸[s]2𝜸[s]1=uUpu𝜸[u]2P=uU(pu/P)𝜸[u]2.

To sum up, 𝐷𝑒𝑐(𝜸[s])=uU(pu/P)𝜸[u] is a convex combination of 𝜸[u] where uU.

Figure 3: Illustrating the meaning of Decrement.

5.4 The subformula 𝑺𝒊𝒎

Recall that

𝑆𝑖𝑚(𝑍𝑒𝑟𝑜Z𝑆𝑡𝑒𝑝,)(¬𝑍𝑒𝑟𝑜P𝑆𝑡𝑒𝑝,)

where

𝑆𝑡𝑒𝑝, i=02ri,𝒜(ri,𝒜𝚄=1rsuci,,Updatei,,)

The purpose of the ri,𝒜𝚄=1rsuci,, 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 Updatei, constructed below, let us assume that s𝑆𝑡𝑒𝑝, where s is a state reachable form a state satisfying φ (in particular, sStruct). We distinguish two subcases.

𝑰𝒏𝒔 updates the counter by dec.

In this case, Updatei,, is similar to Decrement. We define the set U of all states u such that urS(i), and pu>0, where pu is the probability of all runs π initiated in s such that π visits u and all states preceding this visit satisfy ri,.

The formula Updatei,, ensures that if s¬𝑍𝑒𝑟𝑜, then 𝐷𝑒𝑐(𝜸[s]) is a positive convex combination of 𝜸[u] where uU. In addition, it ensures that if s𝑍𝑒𝑟𝑜, then 𝒛 is a positive convex combination of 𝜸[u] where uU. We put Updatei,,UDeci,, where

UDeci,, 𝑍𝑒𝑟𝑜(𝙶=𝒛1(ri,rS(i),aS(i),)𝙶=𝒛2(ri,rS(i),bS(i),)) (2)
¬𝑍𝑒𝑟𝑜(UCopyi,,𝑈𝑆𝑢𝑐𝑐i,,) (3)

where

UCopyi,, 𝙶=δ(ri,ai,a¯i,ci,)𝙵=δ(rS(i),ci,)
𝑈𝑆𝑢𝑐𝑐i,, 𝙵=λ(bS(i),cS(i),dS(i),′′=1mrS2(i),′′)
𝙵=λ(bi,cS(i),dS(i),′′=1mrS2(i),′′)

By using similar arguments as in Section 5.3, it is easy to verify that

  • if sUDeci,,¬𝑍𝑒𝑟𝑜, then 𝐷𝑒𝑐(𝜸[s])=uU(pu/P)𝜸[u];

  • if sUDeci,,𝑍𝑒𝑟𝑜, then 𝒛=uU(pu/P)𝜸[u].

𝑰𝒏𝒔 updates the counter by inc.

Let V be the set consisting of all v such that vai,a¯i, and qv>0, where qv is the probability of all runs π initiated in s such that π visits v and all states preceding this visit satisfy ri,. Furthermore, let W be the set consisting of all w such that wbi,ci,di,rS(i), and qw>0, where qw is the probability of all runs π initiated in s such that π visits w and all states preceding this visit satisfy ri,. The formula Updatei,, ensures the following:

  • 𝐼𝑛𝑐(𝜸[s]) is a positive convex combination of 𝜸[w] where wW.

  • If s¬𝑍𝑒𝑟𝑜, then 𝐷𝑒𝑐(𝜸[s]) is a positive convex combination of 𝜸[v] where vV.

We put Updatei,,UInci,, where UInci,, is the following formula:

𝙶=λ((ri,j=02RjrS(i),aS(i),a¯S(i),j=02Aj)¬K¬ai,¬a¯i,) (4)
𝙶=ϱ((ri,j=02RjrS(i),a¯i,j=02BjbS(i),)¬ai,(Ka¯i,)) (5)
𝙶=ϱ((ri,j=02Rja¯i,j=02(Ejbi,))(Ka¯i,)) (6)
¬𝑍𝑒𝑟𝑜𝙶=λ(ri,ai,a¯i,)j=02(AjK)) (7)
¬𝑍𝑒𝑟𝑜𝙶=δ((ri,ci,j=02(Rjai,)j=02(Rja¯i,)j=02Bj)(Kci,)) (8)
¬𝑍𝑒𝑟𝑜𝙶=δ(ri,bi,ci,) (9)

The meaning of UInci,, is illustrated in Fig. 4. Suppose sUInci,,. Every subformula of UInci,, specifies the probability of visiting a state of a certain family by a run initiated in s. In Fig. 4, these families are indicated by colored shapes (some states belong to multiple families).

  • The subformula (4) says that the probability of reaching a state of the yellow circle family is equal to λ, i.e., wWpw𝜸[w]1=λ. Since PW=wWpw=(1𝜸[s]1), we obtain that

    𝐼𝑛𝑐(𝜸[s])1=λ1𝜸[s]1=wWpw𝜸[w]1PW=wW(pw/PW)𝜸[w]1
  • The subformulae (5) and (6) say that the probabilities of reaching a state of the blue square and the red star families are equal to ϱ. Consequently, wWpw𝜸[w]2=𝜸[s]2λ (this also explains the purpose of the subformula Lambda, see Section 5.1). This implies

    𝐼𝑛𝑐(𝜸[s])2=𝜸[s]2λ1𝜸[s]1=wWpw𝜸[w]2PW=wW(pw/PW)𝜸[w]2
  • If s¬𝑍𝑒𝑟𝑜, then the subformula (7) says that the probability of reaching a state of the green diamond family is equal to λ. Hence, vVpv(1𝜸[v]1)=λ. Since PV=vVpv=𝜸[s]1, we obtain

    𝐷𝑒𝑐(𝜸[s])1=𝜸[s]1λ𝜸[s]1=𝜸[s]1vVpv(1𝜸[v]1)PV=vV(pv/PV)𝜸[v]1
  • If s¬𝑍𝑒𝑟𝑜, then the subformulae (8) and (9) say that the probabilities of reaching a state of the brown triangle and the black semicircle family are equal to δ. This implies vVpv𝜸[v]2=𝜸[s]2. Hence,

    𝐷𝑒𝑐(𝜸[s])2=𝜸[s]2𝜸[s]1=vVpv𝜸[v]2PV=vV(pv/PV)𝜸[v]2.
Figure 4: Illustrating the meaning of Updatei,, when 𝐼𝑛𝑠 updates the counter by inc. The markers are in boldface, and ‘*’ indicates an index j{0,1,2}. The colored shapes indicate the families of states used in the subformulae of UInci,,. Note that the probability of certain transitions is equal to λ due to the subformula Lambda.

5.5 Justifying the correctness of 𝝋𝓜

We claim that φ is satisfiable iff has a recurrent computation, i.e.,

  • if tφ, then there is a run π initiated in t 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 m instructions.

Let 1,2 be non-deterministic one-counter machines obtained from by changing every instruction of form

Ck=0?Z : P:update1,update2

into

C=0?Z : P:update

where updateupdate1 for 1 and updateupdate2 for 2. Observe that 1 and 2 do not simulate in any reasonable sense.

Consider the formulae φ1 and φ2 constructed for 1 and 2 in the way described in the previous sections, where the underlying sets 𝒜1 and 𝒜2 of atomic propositions are disjoint. For every subformula Form constructed in the previous sections, we use Form1 and Form2 to denote the corresponding formulae of φ1 and φ2, respectively.

Intuitively, the formula φ is “basically” the conjunction of φ1 and φ2 with some additional synchronization. First, for every {1,,m}, let NewZero be the formula defined as follows:

  • If the counter tested for zero in 𝐼𝑛𝑠 is C1, then NewZero𝑍𝑒𝑟𝑜1.

  • If the counter tested for zero in 𝐼𝑛𝑠 is C2, then NewZero𝑍𝑒𝑟𝑜2.

Recall that φ1 and φ2 contain the subformulae 𝑆𝑖𝑚1 and 𝑆𝑖𝑚2 corresponding to the subformula

𝑆𝑖𝑚(𝑍𝑒𝑟𝑜Z𝑆𝑡𝑒𝑝,)(¬𝑍𝑒𝑟𝑜P𝑆𝑡𝑒𝑝,)

defined in Section 5.4. Let ψ1 and ψ2 be the formulae obtained from φ1 and φ2 by replacing the two 𝑆𝑖𝑚1 and 𝑆𝑖𝑚2 with 𝑁𝑒𝑤𝑆𝑖𝑚1 and 𝑁𝑒𝑤𝑆𝑖𝑚2, where

𝑁𝑒𝑤𝑆𝑖𝑚1 ((NewZero𝑎𝑡2)Z𝑆𝑡𝑒𝑝,1)((¬NewZero𝑎𝑡2)P𝑆𝑡𝑒𝑝,1)
i=02(ri,1𝒜1¬𝑎𝑡2)(ri,1𝒜1𝚄=1rsuci,,1UDeci,,1)
𝑁𝑒𝑤𝑆𝑖𝑚2 ((NewZero𝑎𝑡1)Z𝑆𝑡𝑒𝑝,2)((¬NewZero𝑎𝑡1)P𝑆𝑡𝑒𝑝,2)
i=02(ri,2𝒜2¬𝑎𝑡1)(ri,2𝒜2𝚄=1rsuci,,2UDeci,,2)

Intuitively, replacing 𝑍𝑒𝑟𝑜 with NewZero ensures that the counter tested for zero in 𝑁𝑒𝑤𝑆𝑖𝑚 is indeed the counter tested for zero in 𝐼𝑛𝑠. The reason for adding the third conjunct in 𝑁𝑒𝑤𝑆𝑖𝑚1 and 𝑁𝑒𝑤𝑆𝑖𝑚2 is more subtle. Roughly speaking, we cannot prevent the situation when a state satisfies 𝑎𝑡1 but not 𝑎𝑡2 (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 C1 (or C2).

Observe that ψ1 and ψ2 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 t encoding a configuration (,c1,c2) of can reach a state encoding a successor configuration (,c1,c2). This is enforced by the formula

Sync =1mi=02𝙶=1((ri,1ri,2)=1m𝙶>0((ri,1ri,2)(rS(i),1rS(i),2)aS(i),1))

Technically, Sync says that whenever a state t satisfying ri,1ri,2 is visited, then t has a successor t satisfying rS(i),1rS(i),2 for some . Due to the subformulae Struct1 and Struct2, the state t must be visited form t via a path such that all states except for t satisfy ri,1ri,2. Note that t has a successor satisfying the marker aS(i),1. Hence, the probability of all runs initiated in t satisfying the formula

𝙶((ri,1ri,2)(rS(i),1rS(i),2)aS(i),1)

is positive (we could use other markers instead of aS(i),1).

We put

φψ1ψ2SyncRecurrent

where

Recurrent 𝙶=1(=1m(𝑎𝑡1𝑎𝑡2)𝙵>0(τ(𝑎𝑡1𝑎𝑡2)))

The formula Recurrent enforces the existence of a run representing a τ-recurrent computation of .

We say that a run π=s0,s1, of a Markov chain represents a computation conf0,conf1, of if there is an infinite increasing sequence of indexes j0,j1, such that for every n, the state sjn represents the configuration confn, i.e., if confn=(,c1,c2), then sjn(𝑎𝑡1𝑎𝑡2), 𝜸1[sjn]=𝐼𝑛𝑐c1(𝒛), and 𝜸2[sjn]=𝐼𝑛𝑐c2(𝒛).

Proposition 6.

If sφ, then there exists πRun(s) representing a recurrent computation of .

Proof.

Let 1={ri,1,Ri10i2,1m} and 2={ri,2,Ri20i2,1m}. For a given state t and k{1,2}, we say that t is k-relevant if t satisfies some proposition of k. For a k-relevant state t, we define 𝜸k[t] as the pair of probabilities of satisfying the path formulae Φtk and Ψtk in t, respectively (see Section 5).

Let us fix a state s such that sφ. We put

T={𝜸k[t]k{1,2},t is k-relevant and reachable from s}

It follows directly form the construction of φ that T satisfies the assumptions of Theorem 5.

Consider the sequence of states s0,s1, definite inductively as follows:

  • s0=s. Observe that s encodes the initial configuration (1,0,0) of .

  • Consider the state sj encoding a configuration (,c1,c2) such that sjri,1ri,2. For all k{1,2}, let Uk be the set of all states u such that urS(i),k and pu>0, where pu is the probability of all runs initiated in sj such that w visits u and all states preceding this visit satisfy ri,k. It follows from the construction of φ that the vector 𝒗k representing the counter value obtained from ck by performing updatek is a positive convex combination of a set of vectors YT, where 𝜸k[u]Y for every uUk. By applying the results of Section 4, we obtain that 𝜸k[u]=𝒗k for every uUk. Hence, we can choose sj+1 as an (arbitrary) element of U1U2 which must be non-empty due to Sync. Note that sj+1 encodes a successor configuration of (,c1,c2).

The above sequence s0,s1, 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 sRecurrent.

Proposition 7.

For every recurrent computation of there exist a Markov chain M, a state s of M, and πRun(s) such that sφ and π represents the computation.

A proof of Proposition 7 is relatively simple but technical. It can be found in [8].

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 𝑁𝑒𝑤𝑆𝑖𝑚1 and 𝑁𝑒𝑤𝑆𝑖𝑚2. 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 Σ11-hard, and the finite satisfiability problem for the 𝙵,𝙶-fragment of PCTL is Σ10-hard.

Consequently, the validity problem for the 𝙵,𝙶-fragment is Π11-hard, and the finite validity problem for the 𝙵,𝙶-fragment is Π10-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.