Pith. sign in

REVIEW 4 major objections 6 minor 72 references

Formal Foundations for Controlled Stochastic Activity Networks

T0 review · 4 major / 6 minor · reviewed 2026-08-03 · deepseek-v4-flash

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

Pith's one-line read Controlled Stochastic Activity Networks unify nondeterministic, probabilistic, and stochastic behavior with explicit control policies, and subsume continuous-time Markov decision processes in the exponential case.

desk verdict The CTMDP generalization fails as stated because Definition 5.16 makes exit rates control-independent, and the expressiveness hierarchy is mostly proof sketches. read the letter →

arxiv 2511.12974 v3 pith:FWAGNPPM submitted 2025-11-17 cs.FL cs.LO

Ali Movaghar This is my paper · ORCID
classification cs.FLcs.LO MSC 68Q4568Q6093C65
keywords controlledstochasticactivitynetworkscontrolpoliciesautomata-theoreticsemanticscontinuous-timeMarkovdecisionprocessesprobabilisticautomatalanguagehierarchiesbisimulationformalverification
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

The paper claims that extending Stochastic Activity Networks with explicit control actions yields a single semantic framework for nondeterministic, probabilistic, and stochastic system dynamics alongside policy-driven decision making. It builds a hierarchy of control policies—memoryless, finite-memory, stack-augmented, tape-augmented, and history-dependent—and shows that the languages they accept form a strict chain from regular to recursively enumerable languages, with computable history-dependent policies collapsing to tape-augmented ones. It also asserts that any computable controlled automaton can be realized by a computable controlled activity network, and that in the exponential-timing case the framework reduces to continuous-time Markov decision processes. If correct, this gives safety-critical system designers one compositional formalism in which control, timing, probability, and nondeterminism can be specified and analyzed together, reusing CTMDP verification techniques as a special case.

What carries the argument

The central object is the controlled automaton (Q, A, C, →, Q0), a state-transition system whose transitions are labeled by activities and control actions, together with policies that map histories to control actions. The expressiveness results are carried by augmenting this automaton with memory structures—finite-state memory, a stack, or a tape—so that each policy class becomes a language class. On the stochastic side, the key reduction is the Controlled Markovian Automaton, a compact representation with activity rate function σ(q,a) = ρ(q,a)α(q,a), and the CTMDP constructed in Definition 5.16 by aggregating rates and probabilities over activities for each control action. The modeling-powe

What would settle it

Take a Controlled Markovian Automaton with two timed activities that have very different rates (say σ(q,a1)=1 and σ(q,a2)=100) and non-identical successor distributions for the same control action, construct the CTMDP from Definition 5.16, and compare finite-horizon state-distribution probabilities under every memoryless policy in both models. Any discrepancy would disprove Proposition 5.17 and collapse the claimed CTMDP generalization.

Watch

Extended reading notes

Core claim

The paper's central claim is that adding a finite set of control actions to Stochastic Activity Networks produces a layered family of automata—controlled automata, controlled probabilistic automata, and controlled stochastic automata—whose behavior is governed by policies selecting control actions at activity completions. Its main theorems assert that every computable controlled automaton is isomorphic to the automaton realized by some computable controlled activity network (Theorem 3.13); that the language classes induced by policy types satisfy the strict hierarchy L0 ⊂ LF ⊂ LStack ⊂ LTape = Lcomp_H ⊂ LH (Theorem 3.29), with global unions equal to REG, CFL, and RE; and that a Controlled Ma

Load-bearing premise

The load-bearing premise is Proposition 5.17, which asserts without proof that the state process of a Controlled Markovian Automaton is isomorphic to the state process of the CTMDP built in Definition 5.16; if that isomorphism fails—due to the required normalization Σ_{q'} P(q,a,c,q') = 1 or to a mismatch in how control actions are selected after activity completions—the paper's headline claim that Controlled SANs generalize CTMDPs is not established.

Editorial extensions

If this is right

  • Emptiness for controlled automata is decidable in polynomial time for memoryless and finite-memory policies, decidable for stack-augmented policies, and undecidable for tape-augmented or arbitrary history-dependent policies.
  • For controlled Büchi automata over infinite words, the same policy hierarchy persists, and emptiness is PSPACE-complete for memoryless and finite-memory policies and undecidable for richer policy classes.
  • For controlled probabilistic automata, threshold-based language emptiness is undecidable under history-dependent policies even when the plant is finite, so the probabilistic setting is strictly harder than the nondeterministic one.
  • Finite-state CTMDPs induced by Controlled SANs admit memoryless deterministic optimal policies for expected-total and discounted reward in polynomial time, while time-bounded reachability and reward objectives are PSPACE-complete.
  • For controlled stochastic automata with arbitrary timing distributions, discretized semi-Markov decision processes yield ε-optimal policies via contracting value iteration that converges geometrically.

Reading between the lines

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

  • The unproved Proposition 5.17 is the hinge of the CTMDP subsumption claim: until the state-process isomorphism between Controlled Markovian Automata and the constructed CTMDP is proved, the relationship to CTMDPs is an assertion rather than an established theorem.
  • The hierarchy's strictness is witnessed by classical separating languages interpreted as degenerate probabilistic systems; in genuinely stochastic settings with threshold semantics, those separations may blur, and the paper does not analyze threshold-sensitive collapses.
  • The modeling-power theorem establishes Turing-level expressiveness only through inhibitor gates and large auxiliary subnetworks, suggesting that practical analysis will need to restrict attention to sublanguages that remain algorithmically tractable.
  • If the CTMDP representation is made rigorous, the framework could inherit existing finite-state CTMDP solvers and PAC reinforcement-learning guarantees, but the precise passage from the paper's reward semantics to CTMDP optimal policies requires a fuller argument than the current unproved isomorphism provides.
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

4 major / 6 minor

Summary. The paper introduces Controlled Stochastic Activity Networks (Controlled SANs), an extension of classical SANs in which timed activities are paired with explicit control actions chosen by policies. It presents a layered semantic hierarchy: controlled automata for nondeterministic behavior, controlled probabilistic automata for discrete probabilistic behavior, and controlled stochastic automata for continuous-time behavior. For each layer it defines policy classes (memoryless, finite-memory, stack-augmented, tape-augmented, history-dependent) and claims a strict expressiveness hierarchy over accepted languages, as well as closure and decidability results. It also claims that the framework generalizes DTMDPs and CTMDPs through representation theorems, and that any computable controlled automaton is realizable by a computable controlled activity network (Theorem 3.13, with a proof in Appendix A).

Significance. If the stated results were fully established, the paper would provide a genuinely unifying automata-theoretic framework for control, nondeterminism, probabilistic branching, and stochastic timing, with policy-based analysis and language-theoretic expressiveness classifications. The ambitions are substantial and the high-level structure is plausible: the policy hierarchy is a natural lifting of classical automata-theoretic memory hierarchies, and Theorem 3.13's reliance on the Turing universality of extended Petri nets is a credible strategy. The paper is also honest about many proof sketches and about the distinction between uniform and standard closure. However, the current manuscript contains load-bearing technical errors in the claimed DTMDP and CTMDP representations, and several central hierarchy statements are supported only by sketches or circular references. These issues must be resolved before the framework's advertised generality can be accepted.

major comments (4)
  1. [§5.16–5.17] The claimed generalization of CTMDPs is invalid as stated. In Definition 5.16, λ(q,c) = Σ_a σ(q,a) · Σ_{q'} P(q,a,c,q'). By Definition 4.2, Σ_{q'} P(q,a,c,q')=1 for every (q,a,c), so λ(q,c) = Σ_a σ(q,a), which is independent of c. Thus only CTMDPs whose total exit rate does not depend on the control action can be represented. A one-state CTMDP with λ(q,c1)=1 and λ(q,c2)=10 has no preimage. Proposition 5.17, even if proved, would only establish isomorphism to this restricted subclass, not to general CTMDPs. The abstract and Section 5's claim that Controlled SANs generalize CTMDPs is therefore not supported.
  2. [§4.40–4.41] The DTMDP representation of a controlled probabilistic automaton is also incorrect. Definition 4.40 sets P'(q,c,q') = Σ_{a∈A} P(q,a,c,q'). Since Definition 4.2 normalizes Σ_{q'} P(q,a,c,q')=1 for each (q,a,c), we get Σ_{q'} P'(q,c,q') = |A|, which violates the DTMDP normalization required in Definition 4.39 unless |A|=1. Proposition 4.41, which asserts an isomorphism of state processes, is stated without proof and appears to depend on this invalid construction. This undermines the paper's claim that controlled probabilistic automata generalize DTMDPs.
  3. [§3.29, §4.19, §4.33] The main expressiveness hierarchy results are supported only by proof sketches. Proposition 3.23 explicitly defers to the proof sketch of Theorem 3.29, and Theorem 3.29's proof is itself a sketch relying on examples such as {a^n b^n} and {a^n b^n c^n} without a formal construction showing that no policy in the lower class can accept those languages across all plants. The probabilistic analogues (Theorems 4.19 and 4.33) are likewise asserted by analogy. Since these hierarchies are a central contribution, full proofs or precise citations are needed, not just sketches.
  4. [§3.31] Proposition 3.31's witness argument is not generally valid. The proof assumes that a finite-memory controller enforcing L_p = (a^p)* 'necessarily counts steps mod p', and then derives a controller for L_{p^2}; but a controlled automaton S need not have the structural ability to emit 'a' and 'terminate' as assumed. The construction of L_{p^2} depends on properties of the plant that are not guaranteed by Definition 3.17. Thus the claimed non-realizability of the prime family by any single S is not established.
minor comments (6)
  1. [§3.15] The type of a memoryless policy is given as π:Q→C, but the execution condition ci−1=π(hi) applies π to histories hi=(q0,a0)...(qi−1,ai−1). This is a type mismatch; clarify that the intended argument is the current state (or reindex appropriately).
  2. [§4.13] Definition 4.13 writes Prπ(ρ) with π(hi+1)(c), but memoryless probabilistic policies are defined as π:Q→Dist(C), which cannot accept a history argument. This notational inconsistency appears throughout Section 4 and should be fixed.
  3. [§4.31] Several equalities in Proposition 4.31 appear to be mislabeled: L^{ω,θ}_{Stack}(Uω) is equated with L^{ω,θ}_{H}(U'ω), and L^{ω,θ}_{Tape}(Uω) with L^{ω,θ}_{H}(U'ω), which is not the claimed bisimulation invariance. Check the indices.
  4. [§5.5] Definition 5.5 has tautological-looking lines: 'for any q∈Q and a∈A, F(.|q,a)=F(.|q,a), ρ(q,a)=ρ(q,a), Π(q,a)=Π(q,a)'. This should be a transfer of the stochastic network parameters to the realized automaton state, not an equality of the same symbols.
  5. [§4.9] Definition 4.9 says 'two equivalent controlled automata' but should refer to controlled probabilistic automata; the runs and policies are from U and M′, so the terminology is inconsistent.
  6. [Throughout] There are numerous typos and inconsistently rendered formulas (e.g., 'instatntaneous', 'contol', missing parentheses, mangled set notation such as P(2^{A*}) and duplicated Theorem 4.19/4.20). A careful proofreading pass is needed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the language hierarchy and CTMDP correspondence are definitional or classical, not back-formed from the paper's conclusions.

full rationale

The derivation chain contains no step in which a claimed prediction is equivalent to a fitted input or in which a load-bearing claim is justified only by the author's own prior work. The policy hierarchies (Propositions 3.23, 3.26, Theorems 3.29, 3.51, 4.19, 4.20, 4.33) follow from the definitions of memoryless/finite/stack/tape policies together with standard automata inclusions; strictness is argued via classical witnesses such as non-regular, non-context-free, and non-recursively-enumerable families, not from the conclusions themselves. The modeling-power Theorem 3.13 cites the author's SAN paper [13], but it also relies on external Petri-net/Turing-machine simulation results [8,37], so the self-citation is background material rather than the sole justification. The CMA-to-CTMDP mapping (Definitions 5.12–5.16, Proposition 5.17) is a definitional abstraction: the CTMDP rate and probability functions are explicitly defined from CMA parameters, and the stated state-process isomorphism is a restatement of that construction rather than an independent empirical prediction. Whether that construction covers all CTMDPs (the skeptic's objection that Definition 5.16 forces λ(q,c) to be independent of c) is a correctness and expressiveness question, not circularity: the paper constructs CTMDPs from CMAs, so a representation gap does not mean the conclusion was assumed in its inputs. Proposition 5.17 is stated without proof, which weakens the generalization claim, but an omitted proof is not a circular derivation. No fitted-input-called-prediction, imported uniqueness theorem, or ansatz-smuggled-via-self-citation pattern was found.

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

This is a theory paper; no empirical parameters are fitted. The paper's results rest on standard mathematical background (automata theory, Chomsky hierarchy, measure-theoretic probability, MDP theory) and on domain assumptions about computability and non-explosiveness. The only invented entities are the formal framework and its semantic models.

assumptions (5)
  • domain assumption Extended Petri nets with inhibitor arcs can simulate nondeterministic Turing machines
    Used in the proof of Theorem 3.13 (Appendix A) to establish that any computable controlled automaton is realizable by a controlled activity network; cited to [37,8], not proven in the paper.
  • standard math Classical results of the Chomsky hierarchy and ω-automata: REG/CFL/RE closure properties, Büchi and McNaughton determinization, Cohen-Gold for ω-CFL, analytic sets
    Relied on in Propositions 3.28, 3.34-3.36, 3.57-3.59 and Remarks 3.37, 3.65; no proofs given because they are standard.
  • standard math Kolmogorov extension theorem and measure-theoretic probability
    Used in Definition 4.27 to construct the probability space for controlled probabilistic Büchi automata.
  • standard math Classical MDP/CTMDP optimality results, including existence of stationary deterministic optimal policies, PSPACE-completeness of time-bounded objectives, and value iteration convergence
    Used in Propositions 4.42, 4.44, 5.18, 5.20, 5.23; cited to [16,62,64,65].
  • domain assumption Non-explosive dynamics and bounded measurable rewards are assumed for infinite-state results
    Stated before Proposition 4.44 and in Remark 5.21; guarantees well-defined value functions and existence of optimal or ε-optimal policies.
invented entities (2)
  • Controlled Stochastic Activity Networks (Controlled SANs)
    purpose: Unified formal model for distributed real-time systems combining SANs with explicit control actions, policies, and stochastic timing.
    A new mathematical formalism introduced by the paper; its value is expressiveness, not empirical falsifiability. No independent evidence outside the paper.
  • Controlled stochastic automata / controlled Markovian automata
    purpose: Semantic models underlying Controlled SANs at the stochastic and Markovian levels.
    Defined as automata-theoretic counterparts of the network models; they are formal constructs without external predictions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Foundations for Controlled Stochastic Activity Networks." pith.science (2026). https://pith.science/paper/FWAGNPPM

@misc{pith2026251112974,
  author       = {Pith},
  title        = {Pith review of: Formal Foundations for Controlled Stochastic Activity Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FWAGNPPM}},
  note         = {Machine review of arXiv:2511.12974}
}
read the original abstract

We introduce Controlled Stochastic Activity Networks (Controlled SANs), a formal extension of classical Stochastic Activity Networks that integrates explicit control actions into a unified semantic framework for modeling distributed real-time systems. Controlled SANs systematically capture dynamic behavior involving nondeterminism, probabilistic branching, and stochastic timing, while enabling policy-driven decision-making within a rigorous mathematical framework. We develop a hierarchical, automata-theoretic semantics for Controlled SANs that encompasses nondeterministic, probabilistic, and stochastic models in a uniform manner. A structured taxonomy of control policies, ranging from memoryless and finite-memory strategies to computationally augmented policies, is formalized, and their expressive power is characterized through associated language classes. To support model abstraction and compositional reasoning, we introduce behavioral equivalences, including bisimulation and stochastic isomorphism. Controlled SANs generalize classical frameworks such as continuous-time Markov decision processes (CTMDPs), providing a rigorous foundation for the specification, verification, and synthesis of dependable systems operating under uncertainty. This framework enables both quantitative and qualitative analysis, advancing the design of safety-critical systems where control, timing, and stochasticity are tightly coupled.

Figures

Figures reproduced from arXiv: 2511.12974 by the authors.

Figure 6
Figure 6. In Figure 3, [PITH_FULL_IMAGE:figures/full_fig_p086_6.png] view at source ↗
Figure 1
Figure 1. An example of a simple controlled activity network [PITH_FULL_IMAGE:figures/full_fig_p087_1.png] view at source ↗
Figure 2
Figure 2. Marking of the model after T1 completes via control action c1 in the model of [PITH_FULL_IMAGE:figures/full_fig_p088_2.png] view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: Marking of the model after I2 completes in the model of [PITH_FULL_IMAGE:figures/full_fig_p089_3.png]
Figure 4
Figure 4. Figure 4: Marking of the model after I1 completes in the model of [PITH_FULL_IMAGE:figures/full_fig_p090_4.png]
Figure 5
Figure 5. Figure 5: A controlled activity subnetwork of K corresponding to an activity a and control action c of M. ✒✑ ✓✏ P0 ✲ KQ0 ✒✑ ✓✏ PS ✲ ✛ [PITH_FULL_IMAGE:figures/full_fig_p091_5.png]
Figure 6
Figure 6. Figure 6: A controlled activity subnetwork of K corresponding to Q0 [PITH_FULL_IMAGE:figures/full_fig_p091_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

72 extracted references · 5 canonical work pages

  1. [1]

    C. A. R. Hoare, An Axiomatic Basis for Computer Programming, Com- munications of the ACM 12 (10) (1969) 576–580.doi:10.1145/363235. 363259

    work page doi:10.1145/363235 1969

  2. [2]

    Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering SE-3 (2) (1977) 125–143.doi: 10.1109/TSE.1977.229904

    L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering SE-3 (2) (1977) 125–143.doi: 10.1109/TSE.1977.229904

    arXiv 1977

  3. [3]

    Newcombe, T

    C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, M. Deardeuff, How Amazon Web Services Uses Formal Methods, Com- munications of the ACM 58 (4) (2015) 66–73.doi:10.1145/2699417

    doi:10.1145/2699417 2015

  4. [4]

    Woodcock, P

    J. Woodcock, P. G. Larsen, J. Bicarregui, J. Fitzgerald, Formal Methods: Practice and Experience, ACM Computing Surveys 41 (4) (2009) 19. doi:10.1145/1592434.1592436

    arXiv 2009

  5. [5]

    S. A. Seshia, E. A. Lee, A. L. Sangiovanni-Vincentelli, Formal Methods for Cyber-Physical Systems: Deductions from Practical Deployments, Annual Review of Control, Robotics, and Autonomous Systems 5 (2022) 121–147.doi:10.1146/annurev-control-042920-022320

    work page doi:10.1146/annurev-control-042920-022320 2022

  6. [6]

    Sipser, Introduction to the Theory of Computation, 3rd Edition, Cengage Learning, 2013

    M. Sipser, Introduction to the Theory of Computation, 3rd Edition, Cengage Learning, 2013

    2013

  7. [7]

    R. Alur, D. L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126 (2) (1994) 183–235. 79

    1994

  8. [8]

    Peterson, Petri Nets Theory and the Modeling of Systems, Prentice- Hall Inc., Englewood Cliffs, 1981

    J. Peterson, Petri Nets Theory and the Modeling of Systems, Prentice- Hall Inc., Englewood Cliffs, 1981

    1981

Show all 72 references
  1. [9]

    Hillston, A Compositional Approach to Performance Modelling, Cam- bridge University Press, 1996.doi:10.1017/CBO9780511564324

    J. Hillston, A Compositional Approach to Performance Modelling, Cam- bridge University Press, 1996.doi:10.1017/CBO9780511564324

    1996 doi

  2. [10]

    Hermanns, Interactive Markov Chains, Vol

    H. Hermanns, Interactive Markov Chains, Vol. 2428 of Lecture Notes in Computer Science, Springer, 2002.doi:10.1007/3-540-45804-2

    2002 doi

  3. [11]

    Movaghar, J

    A. Movaghar, J. Meyer, Performability Modeling with Stochastic Activity Networks, in: IEEE Proc. Real-Time Sys. Symp., 1984, pp. 215–224

    1984

  4. [12]

    J. F. Meyer, A. Movaghar, W. H. Sanders, Stochastic Activity Networks: Structure, Behavior, and Application, in: Proc. Int. Workshop on Timed Petri Nets, 1985, pp. 106–115

    1985

  5. [13]

    Movaghar, Stochastic Activity Networks: A New Definition and Some Properties, Scientia Iranica 8 (4) (2001)

    A. Movaghar, Stochastic Activity Networks: A New Definition and Some Properties, Scientia Iranica 8 (4) (2001)

    2001

  6. [14]

    Milner, Communication and Concurrency, Prentice-Hall International, UK, 1989

    R. Milner, Communication and Concurrency, Prentice-Hall International, UK, 1989

    1989

  7. [15]

    Baier, J.-P

    C. Baier, J.-P. Katoen, Principles of Model Checking, MIT Press, 2008

    2008

  8. [16]

    M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dy- namic Programming, Wiley-Interscience, 1994

    1994

  9. [17]

    P. J. Ramadge, W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM Journal on Control and Optimization 25 (1) (1987) 206–230

    1987

  10. [18]

    C. G. Cassandras, S. Lafortune, Introduction to Discrete Event Systems, 2nd Edition, Springer, 2008

    2008

  11. [19]

    Matthes, Zur Theorie der Bedienungsprozesse, in: Trans

    K. Matthes, Zur Theorie der Bedienungsprozesse, in: Trans. 3rd Prague Conf. on Inf. Thy. Stat. Dec. Fct., Prague, 1962, pp. 513–528

    1962

  12. [20]

    Schassberger, Insensitivity of Steady-State Distributions of General- ized Semi-Markov Processes with Speeds, Adv

    R. Schassberger, Insensitivity of Steady-State Distributions of General- ized Semi-Markov Processes with Speeds, Adv. Appl. Prob. 10 (1978) 836–851. 80

    1978

  13. [21]

    C. J. Tomlin, G. J. Pappas, S. S. Sastry, Conflict Resolution for Air Traffic Management: A Study in Multiagent Hybrid Systems, IEEE Transactions on Automatic Control 43 (4) (1998) 509–521.doi:10.1109/9.664150

    1998 doi

  14. [22]

    M. H. A. Davis, Piecewise-Deterministic Markov Processes: A General Class of Non-Diffusion Stochastic Models, Journal of the Royal Statistical Society. Series B (Methodological) 46 (3) (1984) 353–388

    1984

  15. [23]

    Pnueli, R

    A. Pnueli, R. Rosner, On the Synthesis of a Reactive Module, in: Pro- ceedings of POPL, 1989, pp. 179–190

    1989

  16. [24]

    Segala, Modeling and Verification of Randomized Distributed Real- Time Systems, Ph.D

    R. Segala, Modeling and Verification of Randomized Distributed Real- Time Systems, Ph.D. Thesis, MIT, Cambridge, MA, 1995

    1995

  17. [25]

    Thomas, Automata on Infinite Objects, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (1990) 133–191

    W. Thomas, Automata on Infinite Objects, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (1990) 133–191

    1990

  18. [26]

    M. Y. Vardi, P. Wolper, An Automata-Theoretic Approach to Automatic Program Verification, in: Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS’86), 1986, pp. 332–344

    1986

  19. [27]

    M. O. Rabin, Decidability of Second Order Theories and Automata on Infinite Trees, Transactions of the American Mathematical Society 141 (1969) 1–35

    1969

  20. [28]

    Brázdil, J

    T. Brázdil, J. Esparza, A. Kucera, Qualitative reachability in stochastic BPA games, Information and Computation 208 (9) (2010) 922–938

    2010

  21. [29]

    Etessami, M

    K. Etessami, M. Yannakakis, Recursive Markov Decision Processes and Recursive Stochastic Games, in: ICALP, Springer, 2005, pp. 891–903

    2005

  22. [30]

    Etessami, M

    K. Etessami, M. Yannakakis, Recursive Markov Chains, Stochastic Gram- mars, and Probabilistic Pushdown Systems, Journal of the ACM 56 (1) (2009) 1–66

    2009

  23. [31]

    Esparza, S

    J. Esparza, S. Kiefer, M. Luttenberger, Probabilistic Pushdown Au- tomata, Information and Computation 242 (2014) 148–172

    2014

  24. [32]

    E. M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 1999. 81

    1999

  25. [33]

    Kwiatkowska, G

    M. Kwiatkowska, G. Norman, D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, in: CAV, 2011, pp. 585–591

    2011

  26. [34]

    E. M. Hahn, A. Hartmanns, H. Hermanns, J.-P. Katoen, A Compositional Modelling and Analysis Framework for Stochastic Hybrid Systems, in: FORMATS, 2010, pp. 207–222

    2010

  27. [35]

    Dehnert, S

    C. Dehnert, S. Junges, J. Katoen, M. Volk, A Storm is Coming: A Modern Probabilistic Model Checker, in: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24- 28, 2017, Proceedings, Part II, Vol. 10427 of Lecture Notes in Computer ...

    2017

  28. [36]

    D. D. Deavours, G. Clark, T. Courtney, D. Daly, S. Derisavi, J. M. Doyle, W. H. Sanders, P. G. Webster, The Möbius Framework and Its Implementation, IEEE Transactions on Software Engineering 28 (10) (2002) 956–969.doi:10.1109/TSE.2002.1041052

    2002 arXiv

  29. [37]

    Hack, Decidability Questions for Petri Nets, Ph.D

    M. Hack, Decidability Questions for Petri Nets, Ph.D. Thesis, MIT, Cambridge, MA, 1975

    1975

  30. [38]

    J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd Edition, Pearson, 2007

    2007

  31. [39]

    J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Lan- guages, and Computation, Addison-Wesley, 1979

    1979

  32. [40]

    J. R. Büchi, On a Decision Method in Restricted Second-Order Arith- metic, in: Logic, Methodology and Philosophy of Science, Stanford University Press, 1962, pp. 1–11

    1962

  33. [41]

    McNaughton, Testing and generating infinite sequences by a finite automaton, Information and Control 9 (5) (1966) 521–530

    R. McNaughton, Testing and generating infinite sequences by a finite automaton, Information and Control 9 (5) (1966) 521–530

    1966

  34. [42]

    R. S. Cohen, A. Y. Gold, ω-Computations on Turing Machines, in: H. Barkmeyer, C. Koskas (Eds.), Fundamentals of Computation Theory (FCT ’77), Vol. 63 of Lecture Notes in Computer Science, Springer-Verlag, 1978, pp. 135–154

    1978

  35. [43]

    Staiger, ω-Languages, Handbook of Formal Languages, Volume 3: Beyond Words (1997) 339–387

    L. Staiger, ω-Languages, Handbook of Formal Languages, Volume 3: Beyond Words (1997) 339–387. 82

    1997

  36. [44]

    O.Finkel, OntheTopologicalComplexityofInfinitaryRationalRelations, Theoretical Computer Science 308 (1-3) (2003) 437–456

    2003

  37. [45]

    A. S. Kechris, Classical Descriptive Set Theory, Vol. 156 of Graduate Texts in Mathematics, Springer-Verlag, New York, 1995.doi:10.1007/ 978-1-4612-4190-4

    1995

  38. [46]

    Y. N. Moschovakis, Descriptive Set Theory, 2nd Edition, Vol. 155 of Mathematical Surveys and Monographs, American Mathematical Society, Providence, RI, 2009

    2009

  39. [47]

    Safra, On the Complexity ofω-Automata, in: 29th Annual Symposium on Foundations of Computer Science (FOCS), IEEE, 1988, pp

    S. Safra, On the Complexity ofω-Automata, in: 29th Annual Symposium on Foundations of Computer Science (FOCS), IEEE, 1988, pp. 319–327

    1988

  40. [48]

    Francez, A

    N. Francez, A. Pnueli, A Hierarchy of Automata on Infinite Words, Theoretical Computer Science 11 (1980) 177–195

    1980

  41. [49]

    D. E. Muller, Infinite Sequences and Finite Machines, in: Proc. 4th IEEE Symposium on Switching Circuit Theory and Logical Design, IEEE, 1963, pp. 3–16

    1963

  42. [50]

    Landweber, Decision problems forω-automata, Mathemati- cal Systems Theory 3 (4) (1969) 376–384

    Lawrence H. Landweber, Decision problems forω-automata, Mathemati- cal Systems Theory 3 (4) (1969) 376–384

    1969

  43. [51]

    M. Y. Vardi, P. Wolper, Automata-Theoretic Techniques for Modal Logics of Programs, J. Comput. Syst. Sci. 32 (2) (1986) 183–221

    1986

  44. [52]

    Esparza, D

    J. Esparza, D. Hansel, P. Rossmanith, S. Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Science of Computer Program- ming 50 (1–3) (2004) 231–256

    2004

  45. [53]

    Walukiewicz, Pushdown Processes: Games and Model Checking, in: Computer Aided Verification (CAV 2001), Vol

    I. Walukiewicz, Pushdown Processes: Games and Model Checking, in: Computer Aided Verification (CAV 2001), Vol. 2102 of LNCS, Springer, 2001, pp. 62–74

    2001

  46. [54]

    Bouajjani, J

    A. Bouajjani, J. Esparza, O. Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Theoretical Computer Sci- ence 295 (1–3) (2003) 85–107.doi:10.1016/S0304-3975(02)00407-5

    2003 doi

  47. [55]

    K. G. Larsen, A. Skou, Bisimulation through Probabilistic Testing, Information and Computation 94 (4) (1991) 1–28. 83

    1991

  48. [56]

    M. O. Rabin, Probabilistic Automata, Information and Control 6 (3) (1963) 230–245.doi:10.1016/S0019-9958(63)90290-0

    1963 doi

  49. [57]

    Paz, Introduction to Probabilistic Automata, Academic Press, 1971

    A. Paz, Introduction to Probabilistic Automata, Academic Press, 1971

    1971

  50. [58]

    Madani, S

    O. Madani, S. Hanks, A. Condon, On the Undecidability of Probabilis- tic Planning and Related Stochastic Optimization Problems, Artificial Intelligence 147 (1-2) (2003) 5–34

    2003

  51. [59]

    Billingsley, Probability and Measure, 3rd Edition, John Wiley & Sons, New York, 1995

    P. Billingsley, Probability and Measure, 3rd Edition, John Wiley & Sons, New York, 1995

    1995

  52. [60]

    A. N. Kolmogorov, Foundations of the Theory of Probability, Chelsea Publishing Company, 1950

    1950

  53. [61]

    Baier, M

    C. Baier, M. Grösser, N. Bertrand, Probabilisticω-Automata, Journal of the ACM 59 (1) (2012) 1–52

    2012

  54. [62]

    Courcoubetis, M

    C. Courcoubetis, M. Yannakakis, The Complexity of Probabilistic Verifi- cation, Journal of the ACM 42 (4) (1995) 857–907

    1995

  55. [63]

    R. A. Howard, Dynamic Probabilistic Systems, Volume II: Semi-Markov and Decision Processes, John Wiley & Sons, New York, 1971

    1971

  56. [64]

    E. A. Feinberg, A. Shwartz, Handbook of Markov Decision Processes: Methods and Applications, Springer, Boston, MA, 2002

    2002

  57. [65]

    Hernández-Lerma, J

    O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996

    1996

  58. [66]

    L. G. Valiant, A Theory of the Learnable, Communications of the ACM 27 (11) (1984) 1134–1142

    1984

  59. [67]

    M. J. Kearns, S. P. Singh, Near-optimal Reinforcement Learning in Polynomial Time, Machine Learning 49 (2-3) (2002) 209–232

    2002

  60. [68]

    A. L. Strehl, L. Li, E. Wiewiora, J. Langford, M. L. Littman, Rein- forcement Learning in Finite MDPs: PAC Analysis, Journal of Machine Learning Research 10 (2009) 2413–2444

    2009

  61. [69]

    Lattimore, M

    T. Lattimore, M. Hutter, PAC Bounds for Discounted MDPs, Theoretical Computer Science 558 (2014) 125–143. 84

    2014

  62. [70]

    R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 1st Edition, MIT Press, 1998

    1998

  63. [71]

    Shepardson, H

    J. Shepardson, H. Sturgis, Computability of Recursive Functions, Journal of the ACM 10 (2) (1963) 217–255

    1963

  64. [72]

    inhibitor

    M. Minsky, Computation: Finite and Infinite Machine, Prentice-Hall Inc., Englewood Cliffs, 1967. A. Proofs Proof of Theorem 3.13 Proof. Consider the class of activity networks [13] that have only instanta- neous activities, standard gates, and a special type of gates called “i...

    1967

Pith tools

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