Pith. sign in

REVIEW 3 major objections 5 minor 55 references

POPACheck: A Model Checker for Probabilistic Pushdown Automata

T0 review · 3 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read POPACheck is the first model checking tool for probabilistic pushdown automata that supports temporal logic specifications, and it scales beyond toy examples.

desk verdict A real first tool for pPDA temporal-logic model checking, with an honest evaluation; the front-end translation needs a correctness theorem before the numbers can be fully trusted. read the letter →

arxiv 2502.03956 v2 pith:4SH2IBEU submitted 2025-02-06 cs.LO

Francesco Pontiggia , Ezio Bartocci , Michele Chiari This is my paper · ORCID
classification cs.LO MSC 68Q6068Q4568Q87
keywords probabilisticpushdownautomatamodelcheckingoperatorprecedencelanguagestemporallogicprogrammingrecursionnestedqueriesterminationprobabilities
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper presents POPACheck, a tool that claims to be the first model checker for probabilistic pushdown automata (pPDA) that accepts temporal logic specifications. The authors argue that a subclass of pPDA called probabilistic operator precedence automata (pOPA) can express sampling, conditioning, recursive procedures, and nested inference queries, which cover the behaviors of probabilistic programs. POPACheck translates a recursive probabilistic programming language into pOPA and then answers reachability, qualitative, and quantitative queries for LTL and a fragment of POTL. If the claim holds, probabilistic programs with unbounded recursion could be verified against properties that depend on the call stack, such as partial correctness and pre/post-conditioning, without collapsing the program to a finite-state model.

What carries the argument

The central object is the support chain, built from a pOPA by keeping only stack symbols that are never popped; its transition probabilities are conditioned on the stack symbol being permanent, and support edges replace the entire push-pop subrun with a single edge. Building it requires deciding which symbols are never popped, which in turn requires the termination probabilities defined as the least solution of a nonlinear equation system. POPACheck computes these with a semi-algorithm that combines Optimistic Value Iteration (OVI) for numeric upper bounds, an SMT solver for upper-bound certificates, and a positive almost-sure termination check based on expected-runtime linear equations; when a node is neither positively almost-surely terminating nor provably popping, the algorithm reports inconclusive. The precedence matrix Mcall assigns relations so that the pOPA stack mirrors activation frames of a procedural probabilistic language with rejection sampling: a call pushes, a return shifts and pops, an unsatisfied observation unwinds the stack to the nearest query, and ordinary statements leave the stack unchanged. For specifications, the tool translates LTL formulae into separated Büchi automata and POTLfχ formulae into separated operator-precedence Büchi automata, then analyzes the strongly connected components of the synchronized product with the support chain rather than determinizing the automata.

What would settle it

Run a small probabilistic program with nested queries through POPACheck and compare its reported probability for a property against an exact posterior computed by exhaustive enumeration over the program's finite prefix; any mismatch would falsify the claim that the pOPA semantics preserves the program's distribution. Alternatively, exhibit a pPDA that is almost-surely terminating but not positively almost-surely terminating: POPACheck would then output 'inconclusive' on a true yes-instance, showing the semi-algorithm is not complete.

Watch

Extended reading notes

Core claim

The central claim is that temporal-logic model checking of infinite-state probabilistic systems with recursion is implementable in practice: POPACheck is presented as the first tool supporting LTL and POTLfχ specifications on pPDA, and its experiments report that it builds support chains and answers queries on benchmarks with hundreds of thousands to millions of equations. The key construction is the support chain, a finite Markov chain whose states record stack symbols that are never popped, together with the current automaton state; support edges summarize complete subruns in which a stack symbol is pushed and later popped. The tool computes the needed termination probabilities by a semi-algorithm that combines numeric value iteration with certificates for termination and expected runtime, and it avoids automaton determinization by forming separated automata for the specifications and taking a synchronized product with the support chain. On the reported benchmarks, the tool answers qualitative and quantitative queries in times ranging from under a second to about fifteen minutes, including a randomized binary search case whose state space grows with array size and bit width.

Load-bearing premise

The load-bearing premise is that the pOPA semantics with the OPM Mcall faithfully models the behavior of probabilistic programs with nested rejection sampling, including the meaning of observe and query, so that probabilities computed on the pOPA equal the program's actual posterior distribution; the paper assumes this equivalence and cites prior work for the translation rather than proving it.

Editorial extensions

If this is right

  • If the central claim is correct, probabilistic programs with unbounded recursion and nested queries can be verified against LTL properties without bounding recursion depth first.
  • POTLfχ makes context-free properties such as partial correctness and pre/post-conditioning checkable, and POPACheck is the first implementation to do so on pPDA.
  • The separation-based product avoids the doubly exponential determinization blowup, allowing quantitative model checking on products with up to a few million equations.
  • The OVI-based semi-algorithm computes almost-sure termination probabilities in cases where a direct SMT approach times out, keeping termination-probability computation under a second in the reported benchmarks.
  • The reported benchmarks—coordination game, game-playing, virus spread, and randomized binary search—indicate that the tool scales to medium-size probabilistic programs, providing a baseline for later infinite-state verification tools.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The separation-based product appears to generalize: any specification formalisms with separated automata could likely be plugged into POPACheck's product construction, so extending beyond LTL and POTLfχ may be a matter of building separated automata.
  • Because the termination-probability semi-algorithm falls back to 'inconclusive' when a node is almost-surely terminating but not positively almost-surely terminating, there may be natural programs that are verifiable in principle but for which POPACheck returns no answer; finding such a program would be a concrete stress test.
  • The MiniProb-to-pOPA translation is only cited to prior work, not proved here; a formal proof of that translation would be needed to close the gap between the user-facing language and the verified automaton model.
  • The OPM semantics equates rejection sampling with the pOPA's pop behavior; testing POPACheck's answers against exact inference on small generative programs would empirically validate that equivalence.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents POPACheck, a model checker for probabilistic pushdown automata, instantiated on probabilistic Operator Precedence Automata (pOPA). The tool is claimed to be the first pPDA model checker supporting temporal-logic specifications, namely LTL and the fragment POTLfχ. The technical pipeline consists of: (i) a support-chain construction that turns terminating stack segments into edges of a finite Markov chain; (ii) a semi-algorithm for termination probabilities based on Newton iteration, OVI, and Z3 certificates; (iii) a separation-based synchronized product between the support chain and a separated automaton for the formula, avoiding determinization; and (iv) a front-end language MiniProb with recursion, observation, and nested queries that is compiled to pOPA. The experimental evaluation covers four benchmarks (Schelling, Tic-tac-toe, Virus, and Sherwood binary search) and reports qualitative and quantitative results for LTL/POTLfχ formulae.

Significance. If the full pipeline is sound, POPACheck fills a real gap: temporal-logic model checking of infinite-state recursive probabilistic programs has been studied theoretically but, to the best of the reviewers' knowledge, has not previously been implemented. The separation-based product is a valuable practical choice, as it avoids the doubly exponential determinization step common in LTL model checking. The paper also benefits from using external certificate methods (OVI and expected-runtime certificates) rather than fitting parameters to data, and the artifact is publicly available with a CAV Reusable badge. The main risks are concentrated at the front end and at the quantitative layer: the MiniProb-to-pOPA translation is not proved correct in this manuscript, and the quantitative results are reported as approximate point values without error bounds or certificates. These issues are load-bearing for the concrete tool claims, though the pOPA-level algorithms themselves rest on prior theory and are not called into question by these concerns.

major comments (3)
  1. [§2.1 and §4] The correctness of the MiniProb-to-pOPA translation is load-bearing and is not established in the paper. Section 2.1 asserts that the labels call/ret/qry/obs/stm and the OPM Mcall 'have the same effect on the pOPA stack that they have on the stack of activation frames in a high-level procedural probabilistic programming language with rejection sampling,' but Section 4 gives only the MiniProb grammar and no formal semantics, no translation function, and no correctness theorem. In particular, the treatment of observe as pop moves that unwind the stack to the nearest qry frame fixes one particular rejection-sampling semantics (restart the innermost query, leave outer queries unaffected), but the paper does not prove that this coincides with MiniProb's intended posterior distribution, including normalization at query boundaries, ill-defined queries, and the handling of value-result parameters. Since Tables 2–4 report probabilities computed through this compilation, a semantic gap here would invalidate the central claims. If the proof is in the authors' companion paper [40], the present paper should state the precise theorem and explain why it covers the language features used in the benchmarks; otherwise the proof should be supplied.
  2. [§3.2 and Table 4] Quantitative model-checking results are reported as single approximate probabilities (e.g., P ≈ 0.895, 0.906, 0.288) without intervals, error tolerances, or certificate information. The text states that 'We compute bounds for them with OVI,' and OVI as used in [51] can provide certificates, but the paper does not report the computed bounds, their tightness, or whether the displayed '≈' values lie inside those bounds. A verification tool's quantitative output should be reproducible and checkable; as written, a reader cannot tell whether the P column contains certified intervals or heuristic numerical estimates. The paper should either report the bounded intervals or guaranteed error for each quantitative query in Table 4, or explicitly label the P column as an estimate and clearly separate it from the certified qualitative results.
  3. [§3.1, Fig. 4] The support-chain construction is a semi-algorithm whose completeness depends on the implication Jc↑K = 0 ⇒ c is past. Since almost-sure termination does not imply finite expected time, this implication is not generally valid; the paper acknowledges that if the past check fails, 'the whole algorithm is inconclusive.' However, the paper does not report how often this inconclusive case occurred in the experiments, nor does it state which nodes in Tables 3 and 4 were resolved by the positive lower bound versus by the past check. Without this information, it is unclear whether all reported support chains are complete or whether some nodes were silently excluded from the analysis. The authors should report, per benchmark, the number of nodes that required the past check, how many failed it (if any), and what the tool does in that case.
minor comments (5)
  1. [§3.1] The displayed notation for a support (the sequence ending with 'u0 ⇒ uℓ+1') is malformed in the text; please define the push–pop sequence and the double-arrow notation precisely.
  2. [§3.1] The definition of 'past' says a stack symbol is 'popped with probability 1 infinite expected time'; this should read 'in finite expected time' to match the standard definition of positive almost-sure termination.
  3. [§3.1] The exact quantity Jc↑K and its lower bound appear to be denoted by the same symbol Jc↑K in the prose and in Fig. 4; please use distinct notations (for example, an underbar or overbar) to avoid ambiguity.
  4. [Table 4] For the Virus rows Q.6 and Q.7, the quantitative columns contain '?' and 'TO'; the table caption does not explain these symbols, so please clarify whether these entries denote timeouts, unsupported queries, or values that were not computed.
  5. [§2.2] The semantics of the POTLfχ operators #t, χtF, and Utχ is only sketched; since the paper targets a broad model-checking audience, please include an explicit pointer to the exact satisfaction clauses in [10] or add a short formal definition.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found; POPACheck's outputs are computed from an explicitly defined pOPA semantics and cited external algorithms, with no fitted input renamed as a prediction.

full rationale

The paper's derivation chain is not circular. The pOPA semantics in Definition 1 are given as an automaton model, and the termination-probability equations v = f(v) in Section 3.1 are the standard least-fixed-point characterization from prior pPDA/RMC theory [18,4]. The support chain, Definition 2, is a defined finite Markov chain whose correctness is attributed to the authors' own [40]; while this is a self-citation, it is an ordinary theorem citation rather than a by-construction reduction within this paper. The semi-algorithm for deciding membership in the support chain relies on external certificates for positive almost-sure termination [51,52], not on assuming the answer. The separation-based product in Section 3.2 is likewise justified by cited determinization-avoidance results [11,19,40]. The MiniProb-to-pOPA translation is asserted via citation to [40] rather than proved in this paper, but the paper does not define the MiniProb posterior distribution in terms of the pOPA, nor does it fit any parameter to the quantities it later reports. Tables 2 and 4 are computed outputs, not predictions fitted from data. The skeptical concern about translation soundness is a missing correctness proof for the front end, not circularity. No load-bearing step reduces to its own input by definition or by fitted parameter renaming, so the appropriate score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The method has no fitted constants. All numerical tolerances, such as epsilon in the Z3 upper-bound query, are user-chosen precision parameters that do not affect the correctness of the central claim. The axioms are the least-fixed-point semantics of termination probabilities, the soundness of OVI certificates, the expected-runtime characterization of positive almost-sure termination, the faithfulness of the pOPA model for nested queries, and the validity of the separation-based product.

assumptions (5)
  • standard math Termination probabilities of a pPDA are the least non-negative solution of the equation system v = f(v).
    Invoked in Sec 3.1; established in [18,4].
  • domain assumption OVI with certificates computes a sound upper bound for the least solution of the termination probability system.
    Used in Fig 4 and Sec 3.1; relies on [51].
  • domain assumption A node c is positively almost-surely terminating iff the linear expected-runtime equation system has a solution.
    Used in the past check in Sec 3.1; relies on [52].
  • domain assumption The pOPA semantics with the OPM Mcall faithfully models probabilistic programs with nested rejection sampling.
    Central modeling assumption in Sec 2.1; established in [40].
  • domain assumption Separated automata allow a synchronized product that preserves qualitative and quantitative model checking.
    Used in Sec 3.2; relies on [11,19,40].

how reviews work

0 comments
Cite this review

Pith. "Pith review of POPACheck: A Model Checker for Probabilistic Pushdown Automata." pith.science (2026). https://pith.science/paper/4SH2IBEU

@misc{pith2026250203956,
  author       = {Pith},
  title        = {Pith review of: POPACheck: A Model Checker for Probabilistic Pushdown Automata},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4SH2IBEU}},
  note         = {Machine review of arXiv:2502.03956}
}
read the original abstract

We present POPACheck, the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. POPACheck provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Automata (pOPA). pOPA are a class of pPDA that can express all the behaviors of probabilistic programs: sampling, conditioning, recursive procedures, and nested inference queries. On pOPA, POPACheck can solve reachability queries as well as qualitative and quantitative model checking queries for specifications in Linear Temporal Logic (LTL) and a fragment of Precedence Oriented Temporal Logic (POTL), a logic for context-free properties such as pre/post-conditioning.

Figures

Figures reproduced from arXiv: 2502.03956 by the authors.

Figure 1
Figure 1. Sherwood Binary search. The last two decades saw great efforts to￾wards the analysis of probabilistic Pushdown Automata (pPDA) [14,31,5,3,4,6], and the equivalent model of Recursive Markov Chains (RMCs) [16,54,17,18,19,20] as a succinct for￾malism to express infinite-state probabilistic systems and to model probabilistic programs with nested and possibly recursive procedures. However, no existing tool implements the… view at source ↗
Figure 2
Figure 2. OPM Mcall. PRs guide the stack behavior of pOPA, and PRs between state labels completely determine whether the pOPA pushes, updates, or pops a stack symbol. This dependency of the stack behavior on labels, and hence traces, enables the definition of stack-aware context￾free modalities in the specification formalism (POTL), by allowing the definition of a synchronized product between pOPA and a pushdown automaton enc… view at source ↗
Figure 3
Figure 3. Program stub. In the program of [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Overview of the semi-algorithm for building the support chain (SC). – δMA (u, [a, s])(v, [Λ(u), s]) = δshift(u)(v)Jv, [Λ(u), s] ↑K/Ju, [a, s] ↑K for all (u, [a, s]),(v, [Λ(u), s]) ∈ C such that a .= Λ(u); – otherwise, for all (u, α),(v, α′ ) ∈ C, δMA (u, α)(v, α′ ) = (…
Figure 5
Figure 5. Figure 5: Overview of model checking probabilistic programs against POTLfχ formulae. – In the first method, we give v ∗ as a hint to Z3, and obtain v ∗ as a model for v in the query v ∗ ≤ v ≤ v ∗ + ε ∧ v ≥ f(v), for a small positive ε. – The other method employs OVI [51], which …
Figure 6
Figure 6. Figure 6: MiniProb syntax. and the usual arithmetic and Boo￾lean operators, including compar￾isons. Boolean operators handle inte￾gers (0 means false, everything else true). Programs may sample from Bernoulli(e1, e2), which returns 1 with probability p = e1/e2, and 0 with probab…
Figure 7
Figure 7. Figure 7: Schelling. Schelling. We consider an instance of a Schelling coordination game [48,44]. Two agents wish to meet in town but cannot communicate. However, they know perfectly each other’s preferences. Each agent samples both a location according to its preference, and on…
Figure 8
Figure 8. Figure 8: [48] that maximize future rewards by simulating, through nested queries, other players’ turns as the game progresses. We consider tic-tac-toe [48]. A procedure modelling a player’s reasoning first marks uniformly at random a cell between those not taken yet; then it re…
Figure 9
Figure 9. Figure 9: Virus (sketch). Virus. Recursive probabilistic programs encode epidemiological models and general multi-type Branching Processes [17,27] as models of population dynamics in biology. They consist of an unbounded population of susceptible individuals belonging to distinc…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 34 canonical work pages

  1. [40]

    CoRR (2024),https://doi.org/10.48550/arXiv.2404.03515

    Pontiggia,F.,Bartocci,E.,Chiari,M.:Modelcheckingprobabilisticoperatorprece- dence automata. CoRR (2024),https://doi.org/10.48550/arXiv.2404.03515

    arXiv doi:10.48550/arxiv.2404.03515 2024

  2. [51]

    In: TACAS’23

    Winkler, T., Katoen, J.: Certificates for probabilistic pushdown automata via op- timistic value iteration. In: TACAS’23. LNCS, vol. 13994, pp. 391–409. Springer (2023). https://doi.org/10.1007/978-3-031-30820-8_24

    work page doi:10.1007/978-3-031-30820-8_24 2023

  3. [1]

    MIT Press (2008)

    Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)

    2008

  4. [2]

    Baier, C., Kiefer, S., Klein, J., Müller, D., Worrell, J.: Markov chains and unam- biguous automata. J. Comput. Syst. Sci.136, 113–134 (2023).https://doi.org/ 10.1016/J.JCSS.2023.03.005

    doi:10.1016/j.jcss.2023.03.005 2023

  5. [3]

    In: LPAR’08

    Brázdil, T., Brozek, V., Holecek, J., Kucera, A.: Discounted properties of proba- bilistic pushdown automata. In: LPAR’08. LNCS, vol. 5330, pp. 230–242. Springer (2008). https://doi.org/10.1007/978-3-540-89439-1_17

    work page doi:10.1007/978-3-540-89439-1_17 2008

  6. [4]

    Formal Methods Syst

    Brázdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des.43(2), 124–163 (2013). https://doi.org/ 10.1007/s10703-012-0166-0

    work page doi:10.1007/s10703-012-0166-0 2013

  7. [5]

    In: FOCS ’05

    Brázdil, T., Esparza, J., Kucera, A.: Analysis and prediction of the long-run be- havior of probabilistic sequential programs with recursion (extended abstract). In: FOCS ’05. pp. 521–530. IEEE Computer Society (2005). https://doi.org/10. 1109/SFCS.2005.19

    work page 2005

  8. [6]

    Brázdil, T., Kiefer, S., Kucera, A., Vareková, I.H.: Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci.81(1), 288–310 (2015). https://doi.org/10.1016/J.JCSS.2014.06.005

    doi:10.1016/j.jcss.2014.06.005 2015

Show all 55 references
  1. [7]

    In: STOC’88

    Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC’88. pp. 460–467. ACM (1988).https://doi.org/10.1145/62212.62257

    1988

  2. [8]

    ACM Trans

    Chiari, M., Mandrioli, D., Pontiggia, F., Pradella, M.: A model checker for operator precedence languages. ACM Trans. Program. Lang. Syst. 45(3) (2023). https: //doi.org/10.1145/3608443

    2023 doi

  3. [9]

    In: CAV’21

    Chiari, M., Mandrioli, D., Pradella, M.: Model-checking structured context-free languages. In: CAV’21. LNCS, vol. 12760, p. 387–410. Springer (2021).https: //doi.org/10.1007/978-3-030-81688-9_18

    2021 doi

  4. [10]

    Chiari, M., Mandrioli, D., Pradella, M.: A first-order complete temporal logic for structured context-free languages. Log. Methods Comput. Sci.18:3 (2022). https: //doi.org/10.46298/LMCS-18(3:11)2022

    2022 doi

  5. [11]

    In: LPAR’03

    Couvreur, J., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: LPAR’03. LNCS, vol. 2850, pp. 361–375. Springer (2003). https://doi.org/10.1007/978-3-540-39813-4_26

    2003 doi

  6. [12]

    Esparza, J., Kiefer, S., Luttenberger, M.: Computing the least fixed point of pos- itive polynomial systems. SIAM J. Comput. 39(6), 2282–2335 (2010). https: //doi.org/10.1137/090749591

    2010 doi

  7. [13]

    Esparza, J., Kretínský, J., Sickert, S.: A unified translation of linear temporal logic to ω-automata. J. ACM 67(6), 33:1–33:61 (2020). https://doi.org/10.1145/ 3417995

    2020

  8. [14]

    In: LICS’04

    Esparza, J., Kucera, A., Mayr, R.: Model checking probabilistic pushdown au- tomata. In: LICS’04. pp. 12–21. IEEE Computer Society (2004).https://doi. org/10.1109/LICS.2004.1319596

    2004 arXiv

  9. [15]

    In: STOC’12

    Etessami, K., Stewart, A., Yannakakis, M.: Polynomial time algorithms for multi- type branching processesand stochastic context-free grammars. In: STOC’12. pp. 579–588. ACM (2012).https://doi.org/10.1145/2213977.2214030

    2012

  10. [16]

    In: TACAS’05

    Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: TACAS’05. LNCS, vol. 3440, pp. 253–270. Springer (2005). https://doi.org/10.1007/978-3-540-31980-1_17

    2005 doi

  11. [17]

    In: STACS’05

    Etessami, K., Yannakakis, M.: Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. In: STACS’05. LNCS, vol. 3404, pp. 340–352. Springer (2005).https://doi.org/10.1007/978-3-540-31856-9_28 14 Francesco Pontiggia, Ezio Bartocci, and Michele Chiari

    2005 doi

  12. [18]

    Etessami, K., Yannakakis, M.: Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM56(1), 1:1–1:66 (2009).https: //doi.org/10.1145/1462153.1462154

    2009

  13. [19]

    ACM Trans

    Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log.13(2), 12:1–12:40 (2012).https://doi.org/10.1145/ 2159531.2159534

    2012

  14. [20]

    Etessami, K., Yannakakis, M.: Recursive markov decision processes and recursive stochastic games. J. ACM62(2), 11:1–11:69 (2015). https://doi.org/10.1145/ 2699431

    2015

  15. [21]

    Evans, O., Stuhlmüller, A., Salvatier, J., Filan, D.: Modeling agents with proba- bilistic programs (2017),http://agentmodels.org

    2017

  16. [22]

    Floyd, R.W.: Syntactic analysis and operator precedence. J. ACM10(3), 316–333 (1963). https://doi.org/10.1145/321172.321179

    1963

  17. [23]

    Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nat. 521(7553), 452–459 (2015).https://doi.org/10.1038/NATURE14541

    2015 doi

  18. [24]

    In: UAI’08

    Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K.A., Tenenbaum, J.B.: Church: a language for generative models. In: UAI’08. pp. 220–229. AUAI Press (2008)

    2008

  19. [25]

    Goodman, N.D., Tenenbaum, J.B., The ProbMods Contributors: Probabilistic Models of Cognition.http://probmods.org/v2 (2016), accessed: 2025-5-22

    2016

  20. [26]

    In: FOSE’14

    Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic pro- gramming. In: FOSE’14. pp. 167–181. ACM (2014).https://doi.org/10.1145/ 2593882.2593900

    2014

  21. [27]

    Cambridge University Press (2005)

    Haccou, P., Jagers, P., Vatutin, V.A.: Branching processes: variation, growth, and extinction of populations. Cambridge University Press (2005)

    2005

  22. [28]

    Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022). https://doi.org/10.1007/s10009-021-00633-z

    2022 doi

  23. [29]

    ACM Program

    Jacobs, J.: Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. ACM Program. Lang.5(POPL), 1–26 (2021). https://doi.org/10.1145/3434339

    2021 doi

  24. [30]

    ACM Commun

    Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3/4), 104–105 (2012). https://doi.org/10.1145/2429135. 2429155

    2012 doi

  25. [31]

    Kucera, A., Esparza, J., Mayr, R.: Model checking probabilistic pushdown au- tomata. Log. Methods Comput. Sci. 2(1) (2006). https://doi.org/10.2168/ LMCS-2(1:2)2006

    2006

  26. [32]

    In: CAV’11

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilis- tic real-time systems. In: CAV’11. LNCS, vol. 6806, pp. 585–591. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    2011 doi

  27. [33]

    Computer Science Review27, 61–87 (2018).https://doi.org/ 10.1016/j.cosrev.2017.12.001

    Mandrioli, D., Pradella, M.: Generalizing input-driven languages: Theoretical and practical benefits. Computer Science Review27, 61–87 (2018).https://doi.org/ 10.1016/j.cosrev.2017.12.001

    2018 doi

  28. [34]

    Jones & Bartlett Publishers (2007)

    McConnell, J.: Analysis of algorithms. Jones & Bartlett Publishers (2007)

    2007

  29. [35]

    In: TACAS 2008

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/ 978-3-540-78800-3_24

    2008

  30. [36]

    ACM Trans

    Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Con- ditioning in probabilistic programming. ACM Trans. Program. Lang. Syst.40(1), 4:1–4:50 (2018). https://doi.org/10.1145/3156018 POPACheck: A Model Checker for Probabilistic Pushdown Automata 15

    2018 doi

  31. [37]

    In: LICS’16

    Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS’16. pp. 672–681. ACM (2016).https://doi.org/ 10.1145/2933575.2935317

    2016

  32. [38]

    In: FOCS ’77

    Pnueli, A.: The temporal logic of programs. In: FOCS ’77. pp. 46–57. IEEE Com- puter Society (1977).https://doi.org/10.1109/SFCS.1977.32

    1977 doi

  33. [39]

    A model checking tool for operator precedence languages on omega-words

    Pontiggia, F.: POMC. A model checking tool for operator precedence languages on omega-words. Master’s thesis, Politecnico di Milano (2021),http://hdl.handle. net/10589/176028

    2021

  34. [41]

    In: SEFM’21

    Pontiggia, F., Chiari, M., Pradella, M.: Verification of programs with excep- tions through operator precedence automata. In: SEFM’21. LNCS, vol. 13085, pp. 293–311. Springer, Berlin, Heidelberg (2021). https://doi.org/10.1007/ 978-3-030-92124-8_17

    2021

  35. [42]

    In: Globerson, A., Silva, R

    Rainforth, T.: Nesting probabilistic programs. In: Globerson, A., Silva, R. (eds.) UAI ’18. pp. 249–258. AUAI Press (2018), http://auai.org/uai2018/ proceedings/papers/92.pdf

    2018

  36. [43]

    Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, parts I–III. J. Symb. Comput.13(3), 255–352 (1992).https: //doi.org/10.1016/S0747-7171(10)80003-3

    1992 doi

  37. [44]

    Harvard University Press (1980)

    Schelling, T.C.: The Strategy of Conflict. Harvard University Press (1980)

    1980

  38. [45]

    Scontras, G., Tessler, M.H., Franke, M.: Probabilistic language understanding: An introduction to the Rational Speech Act framework.https://www.problang.org/, accessed: 2025-5-22

    2025

  39. [46]

    Seaman, I.R., van de Meent, J.W., Wingate, D.: Nested reasoning about au- tonomous agents using probabilistic programs (2020), https://arxiv.org/abs/ 1812.01569

    2020 arXiv

  40. [47]

    Stewart, A., Etessami, K., Yannakakis, M.: Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one- counter automata. J. ACM62(4), 30:1–30:33 (2015).https://doi.org/10.1145/ 2789208

    2015

  41. [48]

    Cognitive Systems Research 28, 80–99 (2014).https://doi.org/10.1016/J.COGSYS.2013.07.003

    Stuhlmüller, A., Goodman, N.D.: Reasoning about reasoning by nested condi- tioning: Modeling theory of mind with probabilistic programs. Cognitive Systems Research 28, 80–99 (2014).https://doi.org/10.1016/J.COGSYS.2013.07.003

    2014 doi

  42. [49]

    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994).https://doi.org/10.1006/INCO.1994.1092

    1994

  43. [50]

    In: FOSSACS’22

    Winkler, T., Gehnen, C., Katoen, J.: Model checking temporal properties of re- cursive probabilistic programs. In: FOSSACS’22. LNCS, vol. 13242, pp. 449–469. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_23

    2022 doi

  44. [52]

    In: LICS’23

    Winkler, T., Katoen, J.: On certificates, expected runtimes, and termination in probabilistic pushdown automata. In: LICS’23. pp. 1–13 (2023). https://doi. org/10.1109/LICS56636.2023.10175714

    2023

  45. [53]

    In: TACAS’07

    Wojtczak,D.,Etessami,K.:PReMo:Ananalyzerforprobabilisticrecursivemodels. In: TACAS’07. LNCS, vol. 4424, pp. 66–71. Springer (2007).https://doi.org/ 10.1007/978-3-540-71209-1_7

    2007 doi

  46. [54]

    In: QEST’05

    Yannakakis,M.,Etessami,K.:CheckingLTLpropertiesofrecursiveMarkovchains. In: QEST’05. pp. 155–165. IEEE (2005).https://doi.org/10.1109/QEST.2005.8 16 Francesco Pontiggia, Ezio Bartocci, and Michele Chiari

    2005 doi

  47. [55]

    reasoning about reasoning

    Zhang, Y., Amin, N.: Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recur- sion. ACM Program. Lang. 6(POPL), 1–28 (2022). https://doi.org/10.1145/ 3498677

    2022

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.