pith. sign in

arxiv: 2511.11545 · v2 · submitted 2025-11-14 · 💻 cs.GT

Incremental Data-Driven Policy Synthesis via Game Abstractions

Irmak Sa\u{g}lam , Mahdi Nazeri , Alessandro Abate , Sadegh Soudjani , Anne-Kathrin Schmuck This is my paper

Pith reviewed 2026-05-17 22:00 UTC · model grok-4.3

classification 💻 cs.GT
keywords data-driven controlgame abstractionsincremental synthesisstochastic dynamical systemstemporal logicwinning regionspolicy synthesis2.5-player games
0
0 comments X

The pith

Incremental data updates expand winning regions monotonically in abstracted stochastic games for control synthesis.

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

This paper develops a data-driven method to synthesize control policies for unknown stochastic dynamical systems that must satisfy temporal logic objectives. It constructs and refines finite stochastic game abstractions from accumulating samples by updating reachable-set approximations for each state-action pair. The central result is that these refinements are monotonic: under-approximations grow, over-approximations shrink, and the winning region therefore expands. This property supports an incremental solver that updates the winning region and policy without re-solving the entire game from scratch each time new data arrives.

Core claim

Under appropriate continuity assumptions the unknown dynamics are abstracted into a finite 2.5-player stochastic game graph. As new data samples arrive, refinements to the under- and over-approximations of reachable sets induce structural changes in the game graph; these changes are inherently monotonic, so the winning region for the given temporal logic objective expands. The authors equip the nodes of this graph with an objective-induced ranking function and employ a rank-lifting procedure that uses customized DAG-like subgames (gadgets) to perform the updates efficiently.

What carries the argument

Objective-induced ranking function on game nodes together with customized DAG-like subgames inside a rank-lifting algorithm that incrementally updates the winning region.

If this is right

  • New data samples can only enlarge the set of initial states from which a satisfying control policy exists.
  • Control policies and winning regions can be maintained online by local updates rather than global re-computation.
  • Numerical case studies show substantial computational savings relative to re-solving the full game after every data batch.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same monotonic-update structure could be exploited in other abstraction-based synthesis or verification tasks that accumulate data over time.
  • Active selection of the next data samples could be guided by the current ranking function to accelerate expansion of the winning region.
  • The approach may extend to partially observable or hybrid systems if analogous monotonicity properties can be established for their abstractions.

Load-bearing premise

The unknown system dynamics must satisfy continuity assumptions sufficient to produce a reliable finite stochastic game abstraction from finite data samples.

What would settle it

A concrete counter-example in which adding fresh data samples causes the computed winning region to shrink or remain unchanged, even though the reachable-set approximations have been refined, would falsify the monotonicity claim.

Figures

Figures reproduced from arXiv: 2511.11545 by Alessandro Abate, Anne-Kathrin Schmuck, Irmak Sa\u{g}lam, Mahdi Nazeri, Sadegh Soudjani.

Figure 1
Figure 1. Figure 1: Overview of (A) incremental synthesis, (B) motivating example, and (C) end-to-end data-driven synthesis. Our con [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Unknown function f(x∗, u∗) (black), two noisy observations x1, x2 (small squares) and learned lower and upper bounds ˇf(x∗, u∗|D2), ˆf(x∗, u∗|D2) (dashed). Approximate Reachable Sets We now derive over- and underapproximations of abstract reachable states from the learned bounds via Eq. 2 (cf [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Gray areas indicate insufficient data and are ini [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Execution time of incremental lifting (blue dots) [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The figure represents the outgoing edges of a state [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Simplified cofair coBuchi gadgets for ¨ v ∈ V f \ B (left) and v ∈ V f∩B (right). Doubly encircled nodes denote the coBuchi nodes. ¨ Given the cofair coBuchi game ¨ ⟨Gcf , Inf(B)⟩, the gadget game ⟨G′ , Inf(B′ )⟩ where G′ = (V ′ , V ′ 0 , V ′ 1 , E′ ) is obtained by replacing each fair node v in Gcf with one of the gadgets given in [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 8
Figure 8. Figure 8: Green denotes the goal region; black denotes ob [PITH_FULL_IMAGE:figures/full_fig_p022_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Left: Gray cells indicate regions with sparse [PITH_FULL_IMAGE:figures/full_fig_p022_9.png] view at source ↗
read the original abstract

We address the synthesis of control policies for unknown discrete-time stochastic dynamical systems to satisfy temporal logic objectives. We present a data-driven, abstraction-based control framework that integrates online learning with novel incremental game-solving. Under appropriate continuity assumptions, our method abstracts the system dynamics into a finite stochastic (2.5-player) game graph derived from data. Given a requirement over time on this graph, we compute the winning region -- i.e., the set of initial states from which the objective is satisfiable -- in the resulting game, together with a corresponding control policy. Our main contribution is the construction of abstractions, winning regions and control policies \emph{incrementally}, as data about the system dynamics accumulates. Concretely, our algorithm refines under- and over-approximations of reachable sets for each state-action pair as new data samples arrive. These refinements induce structural modifications in the game graph abstraction -- such as the addition or removal of nodes and edges -- which in turn modify the winning region. Crucially, we show that these updates are inherently monotonic: under-approximations only grow, over-approximations only shrink, and the winning region only expands. We exploit this monotonicity by defining an objective-induced ranking function on the nodes of the abstract game that increases monotonically as new data samples are incorporated. These ranks underpin our novel incremental game-solving algorithm, which employs customized gadgets (DAG-like subgames) within a rank-lifting algorithm to efficiently update the winning region. Numerical case studies demonstrate significant computational savings compared to the baseline approach, which re-solves the entire game from scratch whenever new data samples arrive.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper addresses synthesis of control policies for unknown discrete-time stochastic dynamical systems satisfying temporal logic objectives. It presents a data-driven abstraction framework that constructs finite stochastic (2.5-player) game graphs from data samples, computes winning regions and policies, and updates them incrementally. Refinements of under- and over-approximations of reachable sets induce graph modifications (node/edge additions and removals); the central claim is that these updates are monotonic (under-approximations grow, over-approximations shrink, winning region expands). An objective-induced ranking function on game nodes is defined and used in a rank-lifting algorithm with customized DAG-like gadgets to efficiently update the winning region without full re-solving. Numerical case studies report computational savings versus baseline re-computation.

Significance. If the monotonicity property is rigorously established for general temporal-logic objectives even under node and edge removals, the incremental algorithm could yield substantial efficiency gains for online data-driven control synthesis. The numerical demonstrations of savings are a positive indicator of practicality, and the use of a custom rank-lifting procedure with gadgets is a concrete algorithmic contribution that could be reusable beyond this setting.

major comments (2)
  1. [Abstract] Abstract and the monotonicity claim: the paper states that refinements induce additions or removals of nodes and edges yet the winning region only expands. No explicit argument is visible showing why removals from a shrinking over-approximation cannot contract the winning set for a general temporal-logic objective, even if the ranking function increases on surviving nodes. This is load-bearing for the incremental algorithm's correctness.
  2. [Incremental game-solving algorithm] The description of the rank-lifting algorithm with DAG gadgets: it is not shown how the gadgets are constructed to preserve the monotonic expansion property when both additions and removals occur simultaneously in the same update step.
minor comments (2)
  1. [Abstraction construction] The continuity assumptions used to derive the finite game abstraction from data should be stated more explicitly, including any Lipschitz or modulus-of-continuity requirements.
  2. [Numerical case studies] Numerical case studies would benefit from reporting the exact temporal-logic formulas, state dimensions, and number of data samples at each increment to facilitate reproduction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. The positive assessment of the work's significance is appreciated. We address each major comment below and will revise the manuscript to improve clarity and rigor where needed.

read point-by-point responses

  1. Referee: [Abstract] Abstract and the monotonicity claim: the paper states that refinements induce additions or removals of nodes and edges yet the winning region only expands. No explicit argument is visible showing why removals from a shrinking over-approximation cannot contract the winning set for a general temporal-logic objective, even if the ranking function increases on surviving nodes. This is load-bearing for the incremental algorithm's correctness.

    Authors: We agree that the argument for monotonic expansion of the winning region requires a more explicit and self-contained presentation to address potential contractions from over-approximation shrinkage. The manuscript establishes monotonic growth of under-approximations and shrinkage of over-approximations in Section 3, and argues that the winning region expands in Section 4 by leveraging the objective-induced ranking function that increases on surviving nodes. However, to strengthen this, we will add a dedicated lemma in the revision that formally proves the winning region is non-decreasing for general temporal-logic objectives, accounting for the specific structure of simultaneous node/edge additions and removals induced by the data-driven refinements. revision: yes

  2. Referee: [Incremental game-solving algorithm] The description of the rank-lifting algorithm with DAG gadgets: it is not shown how the gadgets are constructed to preserve the monotonic expansion property when both additions and removals occur simultaneously in the same update step.

    Authors: The rank-lifting procedure with customized DAG-like gadgets is designed to update only affected portions of the game while preserving previously computed winning strategies. The gadgets are constructed to simulate the net structural changes (additions from growing under-approximations and removals from shrinking over-approximations) in a manner that maintains the monotonic increase in the ranking function. We acknowledge that the current exposition in Section 5 does not provide sufficient detail on this construction for simultaneous updates. In the revision, we will expand the description with explicit construction steps and a supporting argument showing that the gadgets preserve the monotonic expansion property. revision: yes

Circularity Check

0 steps flagged

Derivation is self-contained with no circular reductions

full rationale

The paper derives the monotonicity of under-approximations growing, over-approximations shrinking, and winning regions expanding directly from the refinement of reachable-set approximations as new data samples accumulate. This follows from the standard construction of finite stochastic game abstractions under continuity assumptions and the semantics of temporal-logic objectives on the resulting graph, without any reduction to self-defined quantities, fitted parameters renamed as predictions, or load-bearing self-citations. The rank-lifting algorithm with customized DAG gadgets is presented as an algorithmic exploitation of this independently established monotonicity property, building on conventional game-solving methods rather than circularly assuming the target result.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claims rest on continuity assumptions that allow sampled data to produce sound finite game abstractions; no free parameters or new physical entities are introduced.

axioms (1)
  • domain assumption Appropriate continuity assumptions on the system dynamics
    Invoked to guarantee that data-derived transitions form a valid finite stochastic game abstraction.
invented entities (1)
  • Objective-induced ranking function on abstract game nodes no independent evidence
    purpose: To drive the rank-lifting procedure that updates the winning region monotonically
    Introduced as part of the incremental solver; no independent evidence outside the algorithm is provided.

pith-pipeline@v0.9.0 · 5611 in / 1312 out tokens · 37739 ms · 2026-05-17T22:00:17.870542+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

51 extracted references · 51 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

    work page

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

    work page

  3. [3]

    Abate, A.; Katoen, J.-P.; Lygeros, J.; and Prandini, M. 2010. Approximate model checking of stochastic hybrid systems. European Journal of Control, 16(6): 624--641

    work page 2010

  4. [4]

    Abate, A.; Prandini, M.; Lygeros, J.; and Sastry, S. 2008. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 44(11): 2724--2734

    work page 2008

  5. [5]

    P.; Raha, R.; Saglam, I.; and Schmuck, A

    Anand, A.; Nayak, S. P.; Raha, R.; Saglam, I.; and Schmuck, A. 2025. Fair Quantitative Games. In Abdulla, P. A.; and Kesner, D., eds., Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Ca...

    work page 2025

  6. [6]

    Baier, C.; and Katoen, J.-P. 2008. Principles of model checking. MIT press

    work page 2008

  7. [7]

    Banerjee, T.; Majumdar, R.; Mallik, K.; Schmuck, A.-K.; and Soudjani, S. 2023. Fast symbolic algorithms for omega-regular games under strong transition fairness. TheoretiCS, 2

    work page 2023

  8. [8]

    Banse, A.; Romao, L.; Abate, A.; and Jungers, R. M. 2023. Data-driven abstractions via adaptive refinements and a Kantorovich metric. In 2023 62nd IEEE Conference on Decision and Control (CDC), 6038--6043. IEEE

    work page 2023

  9. [9]

    Beliakov, G. 2006. Interpolation of Lipschitz functions. Journal of computational and applied mathematics, 196(1): 20--44

    work page 2006

  10. [10]

    Belta, C.; and Sadraddini, S. 2019. Formal methods for control synthesis: An optimization perspective. Annual Review of Control, Robotics, and Autonomous Systems, 2(1): 115--140

    work page 2019

  11. [11]

    Chatterjee, K.; and Henzinger, M. 2014. Efficient and Dynamic Algorithms for Alternating B\" u chi Games and Maximal End-Component Decomposition. J. ACM, 61(3)

    work page 2014

  12. [12]

    A.; and Langbort, C

    Chekan, J. A.; and Langbort, C. 2023. Safety-Aware Learning-Based Control of Systems with Uncertainty Dependent Constraints. In 2023 American Control Conference (ACC), 1264--1270

    work page 2023

  13. [13]

    H.; Belta, C.; and Tron, R

    Cohen, M. H.; Belta, C.; and Tron, R. 2022. Robust Control Barrier Functions for Nonlinear Control Systems with Uncertainty: A Duality-based Approach. In Proceedings of the IEEE Conference on Decision and Control, volume 2022-Decem, 174--179. ISBN 9781665467612

    work page 2022

  14. [14]

    Fijalkow, N.; Bertrand, N.; Bouyer - Decitre, P.; Brenguier, R.; Carayol, A.; Fearnley, J.; Gimbert, H.; Horn, F.; Ibsen - Jensen, R.; Markey, N.; Monmege, B.; Novotn \' y , P.; Randour, M.; Sankur, O.; Schmitz, S.; Serre, O.; and Skomra, M. 2023. Games on Graphs. CoRR, abs/2305.10546

    work page arXiv 2023

  15. [15]

    Finkbeiner, B. 2016. Synthesis of Reactive Systems. In Esparza, J.; Grumberg, O.; and Sickert, S., eds., Dependable Software Systems Engineering, volume 45 of NATO Science for Peace and Security Series - D: Information and Communication Security , 72--98. IOS Press

    work page 2016

  16. [16]

    Girard, A.; and Pappas, G. J. 2005. Approximate bisimulations for nonlinear dynamical systems. In Proceedings of the 44th IEEE Conference on Decision and Control, 684--689. IEEE

    work page 2005

  17. [17]

    Gracia, I.; Boskos, D.; Laurenti, L.; and Mazo Jr, M. 2023. Distributionally robust strategy synthesis for switched stochastic systems. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, 1--10

    work page 2023

  18. [18]

    Hausmann, D.; Piterman, N.; Sa g lam, I.; and Schmuck, A. 2024. Fair mega-Regular Games. In FoSSaCS (1) , volume 14574 of Lecture Notes in Computer Science, 13--33. Springer

    work page 2024

  19. [19]

    J.; and Zamani, M

    Jagtap, P.; Pappas, G. J.; and Zamani, M. 2020. Control Barrier Functions for Unknown Nonlinear Systems using Gaussian Processes. In Proceedings of the IEEE Conference on Decision and Control, volume 2020-Decem, 3699--3704. ISBN 9781728174471

    work page 2020

  20. [20]

    Jin, Z.; Khajenejad, M.; and Yong, S. Z. 2020. Data-driven model invalidation for unknown Lipschitz continuous systems via abstraction. In 2020 American Control Conference (ACC), 2975--2980. IEEE

    work page 2020

  21. [21]

    Jurdzi \' n ski, M. 2000. Small Progress Measures for Solving Parity Games. In STACS 2000, 290--301. Berlin, Heidelberg: Springer Berlin Heidelberg

    work page 2000

  22. [22]

    Kazemi, M.; Majumdar, R.; Salamati, M.; Soudjani, S.; and Wooding, B. 2024. Data-driven abstraction-based control synthesis. Nonlinear Analysis: Hybrid Systems, 52: 101467

    work page 2024

  23. [23]

    Klarlund, N.; and Kozen, D. 1991. Rabin measures and their applications to fairness and automata theory. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 256--265

    work page 1991

  24. [24]

    Kozen, D. 1983. Results on the Propositional mu-Calculus. Theor. Comput. Sci., 27: 333--354

    work page 1983

  25. [25]

    E.; and Pappas, G

    Kress-Gazit, H.; Fainekos, G. E.; and Pappas, G. J. 2009. Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Transactions on Robotics, 25(6): 1370--1381

    work page 2009

  26. [26]

    Kress-Gazit, H.; Lahijanian, M.; and Raman, V. 2018. Synthesis for robots: Guarantees and feedback for robot behavior. Annual Review of Control, Robotics, and Autonomous Systems, 1(1): 211--236

    work page 2018

  27. [27]

    Lavaei, A.; Soudjani, S.; Abate, A.; and Zamani, M. 2022. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica, 146: 110617

    work page 2022

  28. [28]

    T.; and Slotine, J.-J

    Lopez, B. T.; and Slotine, J.-J. E. 2023. Unmatched Control Barrier Functions: Certainty Equivalence Adaptive Safety. In 2023 American Control Conference (ACC), 3662--3668

    work page 2023

  29. [29]

    Majumdar, R.; Mallik, K.; Rychlicki, M.; Schmuck, A.-K.; and Soudjani, S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In International Conference on Computer Aided Verification, 3--15. Springer

    work page 2023

  30. [30]

    Majumdar, R.; Mallik, K.; Schmuck, A.-K.; and Soudjani, S. 2024. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems, 51: 101430

    work page 2024

  31. [31]

    Makdesi, A.; Girard, A.; and Fribourg, L. 2024. Data-Driven Models of Monotone Systems. IEEE Transactions on Automatic Control, 69(8): 5294--5309

    work page 2024

  32. [32]

    B.; Romao, L.; Calvert, S

    Mathiesen, F. B.; Romao, L.; Calvert, S. C.; Laurenti, L.; and Abate, A. 2024. A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution. arXiv:2410.06662

    work page arXiv 2024

  33. [33]

    B.; Frew, E.; Laurenti, L.; and Lahijanian, M

    Mazouz, R.; Skovbekk, J.; Mathiesen, F. B.; Frew, E.; Laurenti, L.; and Lahijanian, M. 2024. Data-Driven Permissible Safe Control with Barrier Certificates. arXiv:2405.00136

    work page arXiv 2024

  34. [34]

    D.; and Belta, C

    Mehdipour, N.; Althoff, M.; Tebbens, R. D.; and Belta, C. 2023 a . Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges. Automatica, 152: 110692

    work page 2023

  35. [35]

    D.; and Belta, C

    Mehdipour, N.; Althoff, M.; Tebbens, R. D.; and Belta, C. 2023 b . Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges. Automatica, 152: 110692

    work page 2023

  36. [36]

    Nazeri, M.; Badings, T.; Soudjani, S.; and Abate, A. 2025. Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems. Proceedings of Machine Learning Research vol, 283: 1--15

    work page 2025

  37. [37]

    Reissig, G.; Weber, A.; and Rungger, M. 2016. Feedback refinement relations for the synthesis of symbolic controllers. IEEE Transactions on Automatic Control, 62(4): 1781--1796

    work page 2016

  38. [38]

    Salamati, A.; Lavaei, A.; Soudjani, S.; and Zamani, M. 2024. Data-driven verification and synthesis of stochastic systems via barrier certificates. Automatica, 159: 111323

    work page 2024

  39. [39]

    Sa g lam, I.; Schmuck, A.; and Tsyrempilon, M. 2024. A Decremental Algorithm for Fair B \" u chi Games. In Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part I , volume 15054 of Lecture Notes in Computer Science, 89--109. Springer

    work page 2024

  40. [40]

    Sa g lam, I.; and Schmuck, A.-K. 2023. Solving Odd-Fair Parity Games . In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023), volume 284 of Leibniz International Proceedings in Informatics (LIPIcs), 34:1--34:24. Dagstuhl, Germany: Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik. ISBN 97...

    work page 2023

  41. [41]

    S.; Saglam, I.; and Nayak, S

    Schmuck, A.; Thejaswini, K. S.; Saglam, I.; and Nayak, S. P. 2024. Solving Two-Player Games Under Progress Assumptions. In Dimitrova, R.; Lahav, O.; and Wolff, S., eds., Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I , volume 14499 of L...

    work page 2024

  42. [42]

    Sch \"o n, O.; van Huijgevoort, B.; Haesaert, S.; and Soudjani, S. 2024. Bayesian formal synthesis of unknown systems via robust simulation relations. IEEE Transactions on Automatic Control

    work page 2024

  43. [43]

    Soudjani, S.; and Abate, A. 2013. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems, 12(2): 921--956

    work page 2013

  44. [44]

    Tabuada, P. 2009. Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media

    work page 2009

  45. [45]

    Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5: 285--309

    work page 1955

  46. [46]

    Wang, C.; Meng, Y.; Liu, J.; and Smith, S. 2023. Stochastic Control Barrier Functions with Bayesian Inference for Unknown Stochastic Differential Equations. arXiv:2312.12759

    work page arXiv 2023

  47. [47]

    A.; and Egerstedt, M

    Wang, L.; Theodorou, E. A.; and Egerstedt, M. 2018. Safe learning of quadrotor dynamics using barrier certificates. In 2018 IEEE International Conference on Robotics and Automation (ICRA), 2460--2465. IEEE

    work page 2018

  48. [48]

    B.; Smith, R

    Zabinsky, Z. B.; Smith, R. L.; and Kristinsdottir, B. P. 2003. Optimal estimation of univariate black-box Lipschitz functions with upper and lower error bounds. Computers & Operations Research, 30(10): 1539--1553

    work page 2003

  49. [49]

    Zhang, Z.; Ma, C.; Soudijani, S.; and Soudjani, S. 2024. Formal verification of unknown stochastic systems via non-parametric estimation. In International Conference on Artificial Intelligence and Statistics, 3277--3285. PMLR

    work page 2024

  50. [50]

    , " * write output.state after.block = add.period write

    ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...

    work page

  51. [51]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...

    work page