Pith. sign in

REVIEW 4 major objections 7 minor 34 references

A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems

T0 review · 4 major / 7 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read This tutorial establishes a four-step, conservative-by-construction workflow for building finite-state abstractions of cyber-physical systems so that model-checking results transfer back to the original continuous dynamics.

desk verdict A useful tutorial on building conservative abstractions, but the self-loop erasure step breaks the central soundness guarantee—reject as is, though the fix is clear. read the letter →

arxiv 2608.10254 v1 pith:FWCKPET7 submitted 2026-08-10 eess.SY cs.LOcs.SY

Jordan Peper , Krish Kapadia , James Gast , Ethan Howes , Ivan Ruchkin This is my paper · ORCID
classification eess.SYcs.LOcs.SY
keywords conservativeabstractioncyber-physicalsystemslineartemporallogicmodelcheckingPACguaranteeself-looperasureCEGARstate-spacequantization
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 tutorial paper establishes a sound-by-construction workflow for turning a continuous cyber-physical system into a finite-state model whose verification results transfer back to the real system. The central promise is that if the finite abstraction satisfies a suitably lifted temporal-logic specification, then the original system satisfies the original specification, making false positives impossible. The workflow is modular, with interchangeable subroutines for partitioning the state space, building transitions via bounding boxes, polytopes, or sampling with a PAC certificate, purging degenerate behaviors, and lifting LTL specifications through may-must semantics. The authors demonstrate the pipeline on three case studies and show that less conservative transition construction yields higher verification accuracy.

What carries the argument

The load-bearing mechanism is the conservative abstraction pair (Definition 3) combined with the may/must homomorphism rho that translates concrete atomic predicates to may-and-must forms over abstract cells. Definition 3 requires that every concrete state and every concrete one-step transition be represented in the finite transition system, and the translation maps each atomic proposition p to a must-predicate on an abstract cell (true only when every concrete state in the cell satisfies p) and each negation not-p to not of a may-predicate, preserving the implication from abstract satisfaction to concrete satisfaction. The missing-mass upper bound supplies the PAC certificate that underpins the sampling-based transition construction.

What would settle it

Find a cell C and dynamics f such that every trajectory starting in C leaves C within K steps, yet there is some x in C with f(x) also in C. Under the self-loop erasure rule, the transition (C, C) would be deleted even though it represents a genuine one-step behavior, violating Condition 3 of Definition 3. A reader can search for such a cell in a one-dimensional piecewise-linear map, which would refute the erasure rule as stated in Section 7.

Watch

Extended reading notes

Core claim

The paper's central claim is that its four-step pipeline—state-space quantization, conservative transition construction, degenerate-behavior purging, and may-must LTL lifting—produces a conservative abstraction in the sense of Definition 3, for which Definition 5 holds: if the lifted LTL formula is satisfied by all abstract paths from an abstract initial state, then every concrete trajectory from the corresponding concrete initial set satisfies the original formula. Equivalently, the abstraction cannot verify a property that the concrete system violates. For deterministic transition construction using axis-aligned boxes or polytopes, this is an exact guarantee; for sampling-based construction, it holds with a PAC certificate that bounds the probability mass of unobserved transitions.

Load-bearing premise

The subroutine that erases self-loops assumes that if every concrete trajectory starting in a cell exits that cell within K steps, then deleting the cell's self-loop cannot drop any real one-step behavior; if this certification is only asymptotic or probabilistic, the abstraction may lose conservatism.

Editorial extensions

If this is right

  • A model checker working on a finite abstraction can be used to certify safety and liveness properties of a continuous closed-loop system, provided the abstraction is built by the four-step construction.
  • Engineers can choose among bounding-box, polytope, and sampling transition builders as a trade-off between conservatism, runtime, and verification accuracy; the case studies show polytope and sampling methods give higher true-positive rates.
  • Certified self-loop erasure and counterexample-guided abstraction refinement remove spurious behaviors without sacrificing soundness, which improves verification outcomes for liveness specifications.
  • The workflow is a teachable template: each step has interchangeable subroutines, so the overall guarantee transfers as long as the chosen subroutine meets its local certificate.

Reading between the lines

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

  • Beyond the paper, the may-must lifting is not limited to LTL: the same homomorphic translation could lift safety and liveness properties in other branching-time logics by applying may/must at the state-quantifier boundary, though the paper does not develop this.
  • The K-step exit certificate for self-loop erasure is sufficient but not necessary; a testable extension is a weaker certificate that only requires the measure of states with one-step self-transitions to be negligible, which would allow erasing more self-loops while preserving coverage of one-step behaviors.
  • The PAC transition certificate could be generalized to non-uniform sampling distributions via importance weighting, letting abstract builders concentrate samples in high-risk regions of the state space.
  • The pipeline's modularity suggests it can be stress-tested on stochastic cyber-physical systems, where the transition relation would carry probabilistic weights and the lifted specification would need probabilistic semantics.
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 / 7 minor

Summary. The paper proposes a four-step workflow for building finite-state abstractions of deterministic discrete-time cyber-physical systems such that abstract satisfaction of a lifted LTL property implies concrete satisfaction. Step 1 partitions the state space into a rectilinear grid; Step 2 constructs conservative transition relations using axis-aligned bounding boxes, polytopes, or sampling with PAC-style coverage certificates; Step 3 removes self-loops and spurious transitions via certified erasure and counterexample-guided abstraction refinement; Step 4 lifts the LTL specification using may/must semantics. The workflow is demonstrated on three case studies, reporting abstraction metrics, verification times, and true-positive rates. The central claim is that the pipeline is conservative-by-construction and therefore sound for model checking.

Significance. If the soundness claim were correct, this would be a useful tutorial consolidating standard abstraction techniques and offering practical guidance on common pitfalls. The paper is clearly written and gives credit to prior work; it also ships code, uses standard PAC missing-mass bounds, and evaluates the pipeline on three systems with a reference reachability computation. However, the load-bearing soundness argument for self-loop erasure is incorrect, and the sampling-based methods do not produce abstractions that are conservative in the sense of Definition 3. These issues affect the headline conservatism claim and the interpretation of the experimental results, so a substantial revision is needed before the paper can be accepted.

major comments (4)
  1. [Section 7, 'Assured self-loop erasure', Eq. (13)] The criterion that every concrete trajectory originating in Psi(x-hat) exits the cell within K steps does not justify deleting the self-loop (x-hat, sigma, x-hat). Definition 3, condition 2, requires the one-step image f(Psi(x-hat)) to be covered by the successors of x-hat, and a trajectory can remain inside Psi(x-hat) for k < K steps before exiting. The propagation R_{k+1} = R_k intersect AABB(f(R_k)) can have R_1 nonempty while R_K is empty; the certificate proves only that no trajectory survives K steps, not that no state has its one-step image inside the cell. Since the running example uses K=10 and the erasure is applied in all case studies (Tables 2 and 3), the resulting abstraction can under-approximate the concrete dynamics and the implication s-hat models phi-hat => s models phi no longer follows. The erasure criterion should be one-step escape (K=1) or the abstraction must be augmented with additional states or transitions that preserve the intermediate one-step behavior.
  2. [Section 7, 'Sampling-based with PAC guarantee', Eq. (14)] The sample-based erasure certificate is even weaker than the deterministic one. If all N K-length rollouts exit, Eq. (14) only establishes q_tau >= gamma^{1/N} with confidence 1-gamma; it does not establish q_tau = 1. For the running-example parameters (N=100, gamma=0.1), the certified lower bound is only 0.79. Moreover, even a certificate that every trajectory exits within K steps does not rule out one-step images staying in the cell, so deleting the self-loop remains unsound for the same reason as the deterministic erasure. Removing self-loops under this certificate can therefore remove genuine transitions and violate Definition 3.
  3. [Section 6.3, Algorithm 4 and Eq. (11)] The sampling-based transition construction does not produce a conservative abstraction in the sense of Definition 3. The PAC missing-mass certificate guarantees only that all transitions with category probability at least beta under Unif(X) are observed, whereas condition 2 of Definition 3 is universal over x in X and includes transitions from measure-zero sets. Thus an abstraction built by Algorithm 4 can verify a property while a rare concrete trajectory violates it. The abstract's 'conservative-by-construction' claim should be restricted to the AABB and polytope methods, or the paper should explicitly frame sampling as a probabilistic verification method with a residual risk.
  4. [Section 6, Algorithm 2, line 5] The update 'Post_s <- Post_s intersect {x-hat-prime}' should be a union; as printed, the intersection with a singleton either leaves Post_s empty or, if Post_s is nonempty, deletes all previously added successors. Consequently, GetSuccessorsAABB as written always returns the empty set and cannot satisfy condition 2 of Definition 3. Please correct this to 'Post_s <- Post_s union {x-hat-prime}'.
minor comments (7)
  1. [Section 3.2, Definition 3] The text refers to 'Condition 3' but only two conditions are enumerated; the transition condition is condition 2.
  2. [Section 8, Definition 5, Eq. (2)] The antecedent 'Paths_s(x0) models phi-hat' is not well-formed: phi-hat is an LTL formula over abstract states, while Paths_s(x0) is a concrete trajectory or set of trajectories. Please define the induced abstract path via psi and state the implication on that path.
  3. [Section 5, running example] The breakpoints B(1) are listed as {0,4,...,40} and B(2) as {0,5,...,50}, but the state space is X=[0,50] x [0,40]; the labels of B(1) and B(2) appear to be swapped.
  4. [Section 9, Figure 3] The text refers to Figure 3 for TPR versus dimension size, but the figure is not included in the manuscript.
  5. [Section 9.3, Tables 2 and 3] There are typos in the surrounding text ('degenrate', 'imrpovement', 'susbtantial', 'mountain care'); please proofread.
  6. [Section 7, Eq. (14) and running example] The escape probability is denoted q_tau in Eq. (14) and p_tau in the running example; please unify the notation.
  7. [Section 9.2, evaluation metrics] The 'ground truth' satisfaction set is computed by a dense uniform grid; calling it ground truth overstates its accuracy, since this is itself an abstraction.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the pipeline's soundness arguments reduce to explicit definitions and external theorems, not to their own conclusions.

full rationale

The paper's central claim is that the four-step workflow produces a conservative abstraction. The conservatism condition (Definition 3) is a definition, and each successor-construction subroutine is shown to satisfy it by over-approximation: the AABB contains f(Psi(xhat)), the polytope contains f(Psi(xhat)), and every cell intersecting the over-approximation is added to Post, so condition 2 holds by construction rather than by circular assumption. The sampling-based transition method does not claim deterministic conservatism; it imports the McAllester-Schapire missing-mass upper bound (Eq. 10) from external prior work and applies it via Eq. 11, which is a statistical guarantee, not a fitted parameter renamed as a prediction. The LTL lifting in Section 8 defines a homomorphic may/must translation and asserts soundness by construction; this is a theorem to be proved from Definition 5, not a restatement of Definition 5 as its own conclusion. The case studies compare against an independently computed dense-reachability ground truth, so the reported TPR values are not self-referential. No load-bearing self-citation appears; CEGAR is attributed to external prior work (Clarke et al.), and the PAC bounds are attributed to McAllester and Schapire and Good. The most serious technical concern, the assured self-loop erasure in Section 7, is a soundness gap rather than circularity: certifying that trajectories exit a cell within K>1 steps does not imply that one-step images remain outside the cell, so deleting the self-loop can violate condition 2 of Definition 3. That flaw is a logical error in the derivation, but it does not make the derivation equivalent to its inputs by definition or by fitted parameters. Consequently, the paper exhibits no significant circularity.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The workflow's derivations rely on standard PAC inequalities and set-over-approximation assumptions, not on fitted constants. The main ad hoc assumption is the K-step escape criterion for deleting self-loops, which is not implied by the paper's own conservatism definition and is the source of the central soundness failure.

free parameters (3)
  • Abstraction grid count per dimension c^(j) = 100 per dimension (synthetic, mountain car); 60 per dimension (unicycle)
    User-selected partition granularity; experimental results depend on this hand-chosen value.
  • Escape horizon K for self-loop erasure = 50 (experiments), 10 (running example)
    The finite-time escape certificate is relative to K; larger K weakens the one-step justification for erasure.
  • PAC thresholds beta, delta, gamma = 0.01, 0.01, 0.01 (experiments)
    User-set confidence and significance levels; not fitted to data, but they control the strength of the probabilistic certificates.
assumptions (6)
  • domain assumption The state space is rectangular and can be covered by a uniform rectilinear grid
    Step 1 assumes X is a box and defines breakpoints accordingly.
  • domain assumption The concrete system is a discrete-time deterministic transition function f: X to X
    Definition 1; all transition-construction methods propagate f.
  • standard math McAllester-Schapire upper bound on missing mass holds
    Used in Eq. 10 for the PAC transition certificate; cited to McAllester and Schapire.
  • standard math Inclusion-exclusion formula for observing all categories holds
    Used in Eq. 9 for the ground-truth guarantee on sampling-based transitions.
  • ad hoc to paper Finite-time escape within K steps justifies deleting a self-loop while preserving conservatism
    This is the paper's own criterion in Section 7. It does not follow from Definition 3 because one-step transitions inside the cell may still exist for trajectories that exit later.
  • domain assumption The polytope over-approximation PT(f(R)) contains the true image f(R) for nonlinear f
    Algorithm 3 relies on this for conservatism, but the paper does not specify a constructive method for nonlinear dynamics; Eq. 8 forms a convex combination over R, not over f(R), so the definition is ambiguous.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems." pith.science (2026). https://pith.science/paper/FWCKPET7

@misc{pith2026260810254,
  author       = {Pith},
  title        = {Pith review of: A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FWCKPET7}},
  note         = {Machine review of arXiv:2608.10254}
}
read the original abstract

Symbolic model checking is an effective approach for verifying semantically rich temporal-logic properties of cyber-physical systems, but it hinges on discretizing continuous-state dynamics into a finite-state abstraction. To transfer verification guarantees from the abstract model to the concrete CPS, the abstraction must conservatively approximate the concrete state space and behaviors. Hence, model-builders must maintain this soundness while balancing pessimism with tractability. However, they face several common pitfalls such as under-approximating the state space, under-approximating transitions, unsound pruning of "degenerate" behaviors, and improper specification lifting. This tutorial presents a pragmatic, conservative-by-construction workflow for building discrete abstractions of closed-loop dynamical systems. The workflow consists of four modular steps with interchangeable subroutines: (i) state-space partition and abstraction-function design, (ii) conservative transition construction via axis-aligned bounding boxes, polytopes, or sampling with PAC coverage certificates, (iii) mitigation of spurious transitions and self-loops using certified erasure and counterexample-guided abstraction refinement, and (iv) sound lifting of LTL specifications using may-must semantics. We demonstrate the end-to-end pipeline on three case studies and report how these design choices affect abstraction structure, runtime, and verification outcomes.

Figures

Figures reproduced from arXiv: 2608.10254 by the authors.

Figure 1
Figure 1. Overview of the four-step abstraction workflow. 4 Overview of Conservative System Abstraction We start with a brief overview of the conservative system abstraction pipeline (illustrated in [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. A counterexample trajectory admits the sequence of concrete regions (R0, R1, . . .). Counterexample validation iteratively determines the residual intersect￾ing area between the concretized trajectory and its abstract counterpart. In this ex￾ample, this area is 0 by k = 6, validating that the counterexample trajectory is indeed spurious. When τˆ is found to be spurious, CEGAR refines the partition to block the refut… view at source ↗
Figure 3
Figure 3. TPR reported against model dimension size across all case studies and transition-building subroutines. Transition-building subroutines. We analyzed the effects of each transition￾building subroutine (AABB-, polytope-, and sample-based) across the case stud￾ies, reporting the model building and verification runtimes, abstraction metrics, and verification metrics. Abstractions were devised under fixed dimension sizes … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 23 canonical work pages

  1. [1]

    In: Proceedings of the ninth ACM international conference on Embedded software

    Alur, R.: Formal verification of hybrid systems. In: Proceedings of the ninth ACM international conference on Embedded software. pp. 273–278. ACM, Taipei Taiwan (Oct 2011).https://doi.org/10.1145/2038642.2038685,https://dl.acm.org/ doi/10.1145/2038642.2038685

    arXiv 2011

  2. [2]

    Theoretical Computer Science354(2), 250– 271 (Mar 2006).https://doi.org/10.1016/j.tcs.2005.11.026,https://www

    Alur, R., Dang, T., Ivančić, F.: Counterexample-guided predicate ab- straction of hybrid systems. Theoretical Computer Science354(2), 250– 271 (Mar 2006).https://doi.org/10.1016/j.tcs.2005.11.026,https://www. sciencedirect.com/science/article/pii/S0304397505008662

    work page doi:10.1016/j.tcs.2005.11.026 2006

  3. [3]

    ACM Trans

    Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analy- sis of hybrid systems. ACM Trans. Embed. Comput. Syst.5(1), 152–199 (Feb 2006).https://doi.org/10.1145/1132357.1132363,https://dl.acm.org/doi/ 10.1145/1132357.1132363

    work page arXiv 2006

  4. [4]

    MIT Press, Cambridge, MA, USA (Apr 2008)

    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA (Apr 2008)

    work page 2008

  5. [5]

    Statistics & Probability Letters82(6), 1102–1110 (Jun 2012).https://doi.org/10

    Berend, D., Kontorovich, A.: The missing mass problem. Statistics & Probability Letters82(6), 1102–1110 (Jun 2012).https://doi.org/10. 1016/j.spl.2012.02.014,https://www.sciencedirect.com/science/article/ pii/S0167715212000612

    work page 2012

  6. [6]

    Information and Computation98(2), 142–170 (1992)

    Burch,J.R.,Clarke,E.M.,McMillan,K.L.,Dill,D.L.,Hwang,L.J.:Symbolicmodel checking:10 20 states and beyond. Information and Computation98(2), 142–170 (1992)

    work page 1992

  7. [7]

    Casagrande, A.: albertocasagrande/pyModelChecking (Dec 2025),https: //github.com/albertocasagrande/pyModelChecking, original-date: 2015-03- 10T09:22:24Z

    work page 2025

  8. [8]

    ACM Trans

    Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for markov decision processes. ACM Trans. Comput. Logic12(1), 1:1– 1:49 (Nov 2010).https://doi.org/10.1145/1838552.1838553,https://dl.acm. org/doi/10.1145/1838552.1838553

    work page arXiv 2010

Show all 34 references
  1. [9]

    In: Biere, A., Bloem, R

    Chatterjee, K., Chmelík, M., Daca, P.: CEGAR for Qualitative Analysis of Proba- bilistic Systems. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 473–490. Springer International Publishing, Cham (2014).https://doi.org/10. 1007/978-3-319-08867-9_31 Building Con...

    2014

  2. [10]

    (eds.) NASA Formal Methods

    Chen, X., Sankaranarayanan, S.: Reachability Analysis for Cyber-Physical Sys- tems: Are We There Yet? In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. pp. 109–130. Springer International Publishing, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_6

    2022 doi

  3. [11]

    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: An Analyzer for Non- linear Hybrid Systems. In: Hutchison, D., Kanade, T., Kittler, J., Klein- berg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Ran- gan, C., Steffen, B., Sudan, M., Terzopoulos, D., Ty...

    2013 doi

  4. [12]

    Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. International Journal of Foundations of Computer Science 14(04), 583–604 (Aug 2003).https://doi.org/10....

    2003 doi

  5. [13]

    In: Goos, G., Hartmanis, J., Van Leeuwen, J., Garavel, H., Hatcliff, J

    Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Ver- ification of Hybrid Systems Based on Counterexample-Guided Abstraction Re- finement. In: Goos, G., Hartmanis, J., Van Leeuwen, J., Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Const...

    2003 doi

  6. [14]

    In: Emerson, E.A., Sistla, A.P

    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Ab- straction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Ver- ification. pp. 154–169. Springer, Berlin, Heidelberg (2000).https://doi.org/10. 1007/10722167_15

    2000

  7. [15]

    ACM Transactions on Pro- gramming Languages and Systems8(2), 244–263 (1986).https://doi.org/10

    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Pro- gramming Languages and Systems8(2), 244–263 (1986).https://doi.org/10. 1145/5397.5399

    1986

  8. [16]

    01793,http://arxiv.org/abs/2211.01793, arXiv:2211.01793 [eess.SY]

    Coppola, R., Peruffo, A., Mazo, M.: Data-driven Abstractions for Verification of Deterministic Systems (Mar 2023).https://doi.org/10.48550/arXiv.2211. 01793,http://arxiv.org/abs/2211.01793, arXiv:2211.01793 [eess.SY]

    2023 doi arXiv

  9. [17]

    In: 2021 60th IEEE Conference on Decision and Con- trol (CDC)

    Devonport, A., Saoud, A., Arcak, M.: Symbolic Abstractions From Data: A PAC Learning Approach. In: 2021 60th IEEE Conference on Decision and Con- trol (CDC). pp. 599–604. IEEE Press, Austin, TX, USA (Dec 2021).https: //doi.org/10.1109/CDC45484.2021.9683316

    2021

  10. [18]

    In: Raskin, J.F., Thiagarajan, P.S

    Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic Abstraction Refinement for Timed Automata. In: Raskin, J.F., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems. pp. 114–129. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75454-1_10

    2007 doi

  11. [19]

    In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R

    Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of Hybrid Sys- tems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Hand- book of Model Checking, pp. 1047–1110. Springer International Publishing, Cham (2018).https://doi.org/10.1007/978-3-319-1057...

    2018 doi

  12. [20]

    Ameri- can Journal of Mathematics79(3), 497–516 (1957).https://doi.org/10.2307/ 2372560,https://www.jstor.org/stable/2372560, publisher: The Johns Hop- kins University Press

    Dubins, L.E.: On Curves of Minimal Length with a Constraint on Average Cur- vature, and with Prescribed Initial and Terminal Positions and Tangents. Ameri- can Journal of Mathematics79(3), 497–516 (1957).https://doi.org/10.2307/ 2372560,https://www.jstor.org/stable/2372560, pu...

    1957

  13. [21]

    In: Morari, M., Thiele, L

    Fehnker, A., Clarke, E., Jha, S.K., Krogh, B.: Refining Abstractions of Hybrid Systems Using Counterexample Fragments. In: Morari, M., Thiele, L. (eds.) Hy- brid Systems: Computation and Control. pp. 242–257. Springer, Berlin, Heidelberg (2005).https://doi.org/10.1007/978-3-54...

    2005 doi

  14. [22]

    Inter- national Journal on Software Tools for Technology Transfer10(3), 263–279 (Jun 2008).https://doi.org/10.1007/s10009-007-0062-x,http://link.springer

    Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Inter- national Journal on Software Tools for Technology Transfer10(3), 263–279 (Jun 2008).https://doi.org/10.1007/s10009-007-0062-x,http://link.springer. com/10.1007/s10009-007-0062-x

    2008 doi

  15. [23]

    In: Gopalakrishnan, G., Qadeer, S

    Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ri- pado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hy- brid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Veri- fication. pp. 379–395. Springer, Berlin, ...

    2011

  16. [24]

    Good, I.: Turing’s anticipation of empirical bayes in connection with the crypt- analysis of the naval enigma *. Journal of Statistical Computation and Simula- tion66(2), 101–111 (May 2000).https://doi.org/10.1080/00949650008812016, https://doi.org/10.1080/00949650008812016, p...

    doi

  17. [25]

    Annual Reviews in Control33(1), 25– 36 (Apr 2009).https://doi.org/10.1016/j.arcontrol.2009.03.002,https:// www.sciencedirect.com/science/article/pii/S1367578809000078

    Guéguen, H., Lefebvre, M.A., Zaytoon, J., Nasri, O.: Safety verification and reachability analysis for hybrid systems. Annual Reviews in Control33(1), 25– 36 (Apr 2009).https://doi.org/10.1016/j.arcontrol.2009.03.002,https:// www.sciencedirect.com/science/article/pii/S1367578809000078

    2009 doi

  18. [26]

    In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science

    Henzinger, T.: The theory of hybrid automata. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. pp. 278–292 (Jul 1996). https://doi.org/10.1109/LICS.1996.561342,https://ieeexplore.ieee.org/ document/561342, iSSN: 1043-6871

    1996

  19. [27]

    In: Pro- ceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of pro- gramming languages

    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Pro- ceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of pro- gramming languages. pp. 58–70. POPL ’02, Association for Computing Machin- ery, New York, NY, USA (Jan 2002).https://doi.org/...

    2002

  20. [28]

    (eds.) Computer Aided Verification

    Hermanns,H.,Wachter,B.,Zhang,L.:ProbabilisticCEGAR.In:Gupta,A.,Malik, S. (eds.) Computer Aided Verification. pp. 162–175. Springer, Berlin, Heidelberg (2008).https://doi.org/10.1007/978-3-540-70545-1_16

    2008 doi

  21. [29]

    IEEE Transactions on Automatic Control53(1), 287–297 (Feb 2008).https://doi.org/10.1109/TAC.2007.914952, http://ieeexplore.ieee.org/document/4459804/

    Kloetzer, M., Belta, C.: A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications. IEEE Transactions on Automatic Control53(1), 287–297 (Feb 2008).https://doi.org/10.1109/TAC.2007.914952, http://ieeexplore.ieee.org/document/4459804/

    2008

  22. [30]

    Lavaei, A., Frazzoli, E.: Data-Driven Synthesis of Symbolic Abstractions with Guaranteed Confidence (Jun 2022).https://doi.org/10.48550/arXiv.2206. 09397

    2022 doi

  23. [31]

    In: Proceedings of the Thirteenth Annual Conference on Computational Learning Theory

    McAllester, D.A., Schapire, R.E.: On the Convergence Rate of Good-Turing Esti- mators. In: Proceedings of the Thirteenth Annual Conference on Computational Learning Theory. pp. 1–6. COLT ’00, Morgan Kaufmann Publishers Inc., San Fran- cisco, CA, USA (Jun 2000) Building Conserv...

    2000

  24. [32]

    In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

    Rungger, M., Zamani, M.: SCOTS: A Tool for the Synthesis of Symbolic Con- trollers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. pp. 99–104. HSCC ’16, Association for Computing Ma- chinery, New York, NY, USA (Apr 2016).https:...

    2016 doi

  25. [33]

    IFAC Proceedings Volumes44(1), 4546–4551 (Jan 2011).https://doi.org/10.3182/20110828-6-IT-1002.02568,https:// linkinghub.elsevier.com/retrieve/pii/S1474667016443247

    Sloth, C., Wisniewski, R.: Algorithmic Approach to Abstracting Linear Sys- tems by Timed Automata*. IFAC Proceedings Volumes44(1), 4546–4551 (Jan 2011).https://doi.org/10.3182/20110828-6-IT-1002.02568,https:// linkinghub.elsevier.com/retrieve/pii/S1474667016443247

    2011

  26. [34]

    48550/arXiv.2407.17032,http://arxiv.org/abs/2407.17032, arXiv:2407.17032 [cs.LG] 28 J

    Towers, M., Kwiatkowski, A., Terry, J., Balis, J.U., Cola, G.D., Deleu, T., Goulão, M., Kallinteris, A., Krimmel, M., KG, A., Perez-Vicente, R., Pierré, A., Schulhoff, S., Tai, J.J., Tan, H., Younis, O.G.: Gymnasium: A Standard Inter- face for Reinforcement Learning Environmen...

    2025 doi arXiv

Pith tools

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