pith. sign in

arxiv: 2605.00752 · v1 · submitted 2026-05-01 · 📡 eess.SY · cs.LO· cs.SY

HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications

Vishnu Murali , Amin Falah , Ashutosh Trivedi , Majid Zamani This is my paper

Pith reviewed 2026-05-09 19:09 UTC · model grok-4.3

classification 📡 eess.SY cs.LOcs.SY
keywords HyperCertificatesHyperLTLhyperpropertiesdynamical systemsbarrier functionsranking functionsclosure certificatesverification
0
0 comments X

The pith

HyperCertificates enable inductive verification of HyperLTL hyperproperties for discrete-time dynamical systems.

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

The paper introduces a certificate method to check whether discrete-time dynamical systems satisfy HyperLTL formulas, which describe relations among multiple execution traces rather than single-trace behaviors. HyperCertificates consist of two functions: one that models the necessary lookahead over future states and another that combines barrier and ranking functions to enforce the property step by step. Closure certificates handle the lookahead modeling, after which the barrier and ranking arguments reduce verification to inductive conditions that existing solvers can discharge. Readers would care because this extends standard verification techniques to relational specifications such as opacity and privacy without requiring exhaustive comparison of all trace pairs.

Core claim

The authors introduce a functional inductive framework to verify discrete-time dynamical systems against HyperLTL formulae via HyperCertificates consisting of a pair of functions, where the first models the lookahead and the second relies on a combination of barrier and ranking functions. Closure certificates act as the model for this lookahead, allowing barrier and ranking function arguments to provide guarantees against the HyperLTL formulae. The approach is automatable via sum-of-squares optimization and satisfiability modulo theories solvers, and is demonstrated on case studies.

What carries the argument

HyperCertificates, a pair of functions in which the first models lookahead via closure certificates and the second uses barrier and ranking functions to discharge inductive obligations for HyperLTL specifications.

If this is right

  • Hyperproperties such as opacity and privacy can be verified for discrete-time systems by reducing the problem to inductive conditions modulo a lookahead model.
  • Sum-of-squares optimization and SMT solvers become applicable tools for discharging the verification obligations.
  • The separation of lookahead modeling from the barrier-ranking step allows the same framework to handle a range of HyperLTL formulae.
  • Case studies show the method applies directly to concrete dynamical systems without manual trace enumeration.

Where Pith is reading between the lines

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

  • The separation into lookahead and inductive components may suggest similar decompositions for other temporal logics that quantify over multiple traces.
  • If closure certificate construction can be automated further, the overall procedure could scale to larger state spaces than direct model checking.
  • The reliance on barrier and ranking functions opens the possibility of importing synthesis techniques already developed for safety and termination proofs.

Load-bearing premise

That closure certificates can be constructed to capture the lookahead needed for arbitrary HyperLTL formulae and that barrier and ranking functions exist which can be found by SOS or SMT solvers for the given system.

What would settle it

A discrete-time system and HyperLTL formula for which the system satisfies the property yet no HyperCertificate pair exists, or an SOS/SMT solver returns no solution even though such functions are known to exist.

Figures

Figures reproduced from arXiv: 2605.00752 by Amin Falah, Ashutosh Trivedi, Majid Zamani, Vishnu Murali.

Figure 1
Figure 1. Figure 1: An example illustrating the limitations of augmented barrier certificates in verifying opacity. The discrete time system demonstrates a case where one fails to find an augmented barrier to establish opacity, even though the system is opaque. Closure Certificates. To overcome this, we introduce a lookahead variable that encodes a future state that could be visited by the ∀-player. This lookahead aug￾ments t… view at source ↗
Figure 3
Figure 3. Figure 3: A finite state example illustrating the limitations of ∀ ∗∃ ∗ certificates as in Definition5.1 indicating the limitations of our approach. 7. HyperCertificates for General Hyperproperties We now present a set of conditions to verify systems against general HyperLTL formulae. Similarly to the approach for ∀ ∗∃ ∗ hyperproperties, we make use of certificates over the product of the product system and the NBA … view at source ↗
read the original abstract

We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae which are concerned with individual traces of a system, hyperproperties are properties that are concerned with how the traces of a system relate to one another. HyperLTL is an extension of LTL for hyperproperties, and is useful to describe specifications such as opacity, privacy as well as notions of robustness. Our notion of HyperCertificates consists of a pair of functions, where the first models the lookahead, and the second relies on a combination of barrier and ranking functions. We use closure certificates, to act as a model for this lookahead and then rely on barrier and ranking function arguments modulo this lookahead to provide guarantees against HyperLTL formulae. We demonstrate how our approach is automatable via existing techniques such as sum-of-squares optimization (SOS) and satisfiability modulo theories (SMT) solvers. Finally, we demonstrate our approach on some case studies.

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 introduces a functional inductive framework to verify discrete-time dynamical systems against HyperLTL specifications using HyperCertificates, defined as a pair of functions where the first models lookahead via closure certificates and the second combines barrier and ranking functions. The approach is claimed to be automatable via sum-of-squares optimization and SMT solvers, with illustrations on case studies.

Significance. If the framework correctly discharges inductive obligations for a non-trivial class of HyperLTL formulae, it would extend classical barrier/ranking techniques to hyperproperties such as opacity and robustness, with the automation route via SOS/SMT offering a practical strength for control-system verification.

major comments (2)
  1. [Section introducing HyperCertificates and closure certificates] The central claim that closure certificates suffice to model lookahead for arbitrary HyperLTL formulae is load-bearing but unsupported in general. For formulae containing 'eventually' operators under trace quantifiers, the required lookahead can be unbounded or state-dependent, so the inductive step using barrier/ranking functions may not be dischargeable; this needs an explicit restriction on the supported fragment or a proof that finite closure certificates always exist.
  2. [Section on automation via SOS/SMT] No theorem or proof sketch is supplied showing that the HyperCertificate obligations reduce to SOS or SMT problems for the claimed class of formulae; without this, the automation claim cannot be evaluated and the soundness of the inductive framework remains open.
minor comments (2)
  1. [Abstract] The abstract states that the method is demonstrated on case studies but supplies no quantitative metrics, specific HyperLTL formulae, or system dimensions, which weakens the reader's ability to assess practical utility.
  2. [Preliminaries and definitions] Notation for the pair of functions in a HyperCertificate and the precise inductive obligations should be introduced with a small running example before the general case.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. The comments highlight important points regarding the scope of the HyperCertificate framework and the automation claims. We address each major comment below and will incorporate clarifications and additions in the revised manuscript.

read point-by-point responses

  1. Referee: [Section introducing HyperCertificates and closure certificates] The central claim that closure certificates suffice to model lookahead for arbitrary HyperLTL formulae is load-bearing but unsupported in general. For formulae containing 'eventually' operators under trace quantifiers, the required lookahead can be unbounded or state-dependent, so the inductive step using barrier/ranking functions may not be dischargeable; this needs an explicit restriction on the supported fragment or a proof that finite closure certificates always exist.

    Authors: We agree that the general claim for arbitrary HyperLTL is not supported, as unbounded or state-dependent lookahead can arise with 'eventually' operators. The manuscript's examples and definitions target a fragment consisting of safety hyperproperties and bounded-lookahead specifications (e.g., opacity and certain robustness notions) for which finite closure certificates suffice. We will revise the introduction, the HyperCertificate definition, and the main theorem to explicitly restrict to this fragment and state that we do not claim finite closure certificates exist for all HyperLTL formulae. Within the supported fragment the inductive step with barrier and ranking functions is valid. revision: yes

  2. Referee: [Section on automation via SOS/SMT] No theorem or proof sketch is supplied showing that the HyperCertificate obligations reduce to SOS or SMT problems for the claimed class of formulae; without this, the automation claim cannot be evaluated and the soundness of the inductive framework remains open.

    Authors: The HyperCertificate conditions are implications over the system dynamics and the certificate functions; for polynomial dynamics these become polynomial inequalities that reduce to SOS programs, while for general dynamics they become first-order formulas amenable to SMT solvers, consistent with standard barrier-certificate encodings. We will add a new theorem in the automation section that formally states this reduction for the supported HyperLTL fragment, together with a concise proof sketch showing how each inductive obligation maps to an SOS constraint or SMT query. This will make both the automation route and the overall soundness explicit. revision: yes

Circularity Check

0 steps flagged

No circularity: HyperCertificate definition and verification obligations are independently constructed

full rationale

The paper introduces HyperCertificates as an explicit pair of functions (lookahead modeled by closure certificates, verification via barrier/ranking functions) and discharges the resulting inductive obligations using standard SOS/SMT solvers on the given system dynamics. No equation or claim reduces by construction to a fitted parameter, self-definition, or prior self-citation; the framework extends existing LTL barrier techniques to HyperLTL without renaming known results or smuggling ansatzes. The derivation chain remains self-contained against external benchmarks such as HyperLTL semantics and sum-of-squares programming.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on standard assumptions about discrete-time systems and the existence of suitable certificates; no free parameters or invented entities beyond the new certificate notion are described.

axioms (1)
  • domain assumption Discrete-time dynamical systems admit transition functions that can be analyzed inductively.
    Invoked throughout the description of the verification framework.
invented entities (1)
  • HyperCertificates no independent evidence
    purpose: Pair of functions providing inductive guarantees for HyperLTL formulae.
    Newly introduced concept whose existence is asserted by the framework.

pith-pipeline@v0.9.0 · 5496 in / 1216 out tokens · 42479 ms · 2026-05-09T19:09:19.268148+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

144 extracted references · 144 canonical work pages

  1. [1]

    NASA Formal Methods Symposium , pages=

    Automata-based software model checking of hyperproperties , author=. NASA Formal Methods Symposium , pages=. 2023 , organization=

    work page 2023

  2. [2]

    Program Verification: Fundamental Issues in Computer Science , pages=

    Assigning meanings to programs , author=. Program Verification: Fundamental Issues in Computer Science , pages=. 1993 , publisher=

    work page 1993

  3. [3]

    Indiana University Mathematics Journal , volume=

    Positive polynomials on compact semi-algebraic sets , author=. Indiana University Mathematics Journal , volume=. 1993 , publisher=

    work page 1993

  4. [4]

    Annual Reviews in Control , volume=

    On the history of diagnosability and opacity in discrete event systems , author=. Annual Reviews in Control , volume=. 2018 , publisher=

    work page 2018

  5. [5]

    Annual reviews in control , volume=

    Overview of discrete event systems opacity: Models, validation, and quantification , author=. Annual reviews in control , volume=. 2016 , publisher=

    work page 2016

  6. [6]

    2020 IEEE International Conference on Robotics and Automation (ICRA) , pages=

    Hyperproperties for robotics: Planning via HyperLTL , author=. 2020 IEEE International Conference on Robotics and Automation (ICRA) , pages=. 2020 , organization=

    work page 2020

  7. [7]

    IEEE Transactions on Automatic Control , year=

    Verification of Hyperproperties for Dynamical Systems via Barrier Certificates , author=. IEEE Transactions on Automatic Control , year=

    work page

  8. [8]

    Automatica , volume=

    Set invariance in control , author=. Automatica , volume=. 1999 , publisher=

    work page 1999

  9. [9]

    International Conference on Computer Aided Verification , pages=

    Second-order hyperproperties , author=. International Conference on Computer Aided Verification , pages=. 2023 , organization=

    work page 2023

  10. [10]

    and D'Argenio, P

    Barthe, G. and D'Argenio, P. R. and Rezk, T. , year =. Secure information flow by self-composition , booktitle =

    work page

  11. [11]

    International Conference on Computer Aided Verification , pages=

    Algorithms for model checking HyperLTL and HyperCTL , author=. International Conference on Computer Aided Verification , pages=. 2015 , organization=

    work page 2015

  12. [12]

    MGH yper: Checking Satisfiability of HyperLTL Formulas Beyond the \^

    Finkbeiner, Bernd and Hahn, Christopher and Hans, Tobias , booktitle=. MGH yper: Checking Satisfiability of HyperLTL Formulas Beyond the \^. 2018 , organization=

    work page 2018

  13. [13]

    27th International Conference on Concurrency Theory , pages =

    Bernd Finkbeiner and Christopher Hahn , title =. 27th International Conference on Concurrency Theory , pages =. 2016 , volume =

    work page 2016

  14. [14]

    arXiv preprint arXiv:2311.07695 , year=

    Co-buchi barrier certificates for discrete-time dynamical systems , author=. arXiv preprint arXiv:2311.07695 , year=

    work page arXiv

  15. [15]

    Proceedings of the ACM on Programming Languages , volume=

    Induction duality: primal-dual search for invariants , author=. Proceedings of the ACM on Programming Languages , volume=. 2022 , publisher=

    work page 2022

  16. [16]

    2019 18th European control conference (ECC) , pages=

    Control barrier functions: Theory and applications , author=. 2019 18th European control conference (ECC) , pages=. 2019 , organization=

    work page 2019

  17. [17]

    IFAC Proceedings Volumes , volume=

    Constructive safety using control barrier functions , author=. IFAC Proceedings Volumes , volume=. 2007 , publisher=

    work page 2007

  18. [18]

    , publisher =

    Zhou, Kemin and Doyle, John C. , publisher =. Essentials of

    work page

  19. [19]

    Distributed computing , volume=

    Recognizing safety and liveness , author=. Distributed computing , volume=. 1987 , publisher=

    work page 1987

  20. [20]

    Journal of Computer and System Sciences , volume=

    The correctness of programs , author=. Journal of Computer and System Sciences , volume=. 1969 , publisher=

    work page 1969

  21. [21]

    IEEE Transactions on Control of Network Systems , volume=

    Barrier function based collaborative control of multiple robots under signal temporal logic tasks , author=. IEEE Transactions on Control of Network Systems , volume=. 2020 , publisher=

    work page 2020

  22. [22]

    IEEE control systems letters , volume=

    Control barrier functions for signal temporal logic tasks , author=. IEEE control systems letters , volume=. 2018 , publisher=

    work page 2018

  23. [23]

    1982 , publisher=

    Verification of sequential programs: Temporal axiomatization , author=. 1982 , publisher=

    work page 1982

  24. [24]

    Communications of the ACM , volume=

    An axiomatic basis for computer programming , author=. Communications of the ACM , volume=. 1969 , publisher=

    work page 1969

  25. [25]

    arXiv:2405.17304

    Stochastic omega-regular verification and control with supermartingales , author=. arXiv preprint arXiv:2405.17304 , year=

    work page arXiv

  26. [26]

    Autonomous Robots , volume=

    Learning control lyapunov functions from counterexamples and demonstrations , author=. Autonomous Robots , volume=. 2019 , publisher=

    work page 2019

  27. [27]

    International Conference on Computer Aided Verification , pages=

    Latticed k-induction with an application to probabilistic programs , author=. International Conference on Computer Aided Verification , pages=. 2021 , organization=

    work page 2021

  28. [28]

    , booktitle=

    McLean, J. , booktitle=. A general theory of composition for trace sets closed under selective interleaving functions , year=

    work page

  29. [29]

    Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach , year=

    Zhang, Kuize and Yin, Xiang and Zamani, Majid , journal=. Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach , year=

    work page

  30. [30]

    Temporal logic verification of stochastic systems using barrier certificates , Year =

    Jagtap, Pushpak and Soudjani, Sadegh and Zamani, Majid , Booktitle =. Temporal logic verification of stochastic systems using barrier certificates , Year =

    work page

  31. [31]

    IEEE Transactions on Automatic Control , year=

    Formal synthesis of stochastic systems via control barrier certificates , author=. IEEE Transactions on Automatic Control , year=

    work page

  32. [32]

    Game-Theoretic Semantics for Alternating-Time Temporal Logic , year =

    Goranko, Valentin and Kuusisto, Antti and R\". Game-Theoretic Semantics for Alternating-Time Temporal Logic , year =. International Conference on Autonomous Agents & Multiagent Systems , pages =

    work page

  33. [33]

    Overviews on the applications of the Kuramoto model in modern power system analysis , volume=

    Yufeng Guo and Dongrui Zhang and Zhuchun Li and Qi Wang and Daren Yu , journal =. Overviews on the applications of the Kuramoto model in modern power system analysis , volume=. 2021 , publisher=

    work page 2021

  34. [34]

    International Workshop on Hybrid Systems: Computation and Control , pages=

    Safety verification of hybrid systems using barrier certificates , author=. International Workshop on Hybrid Systems: Computation and Control , pages=. 2004 , publisher =

    work page 2004

  35. [35]

    Program Synthesis by Sketching , author =

    work page

  36. [36]

    Principles of model checking , Year =

    Baier, Christel and Katoen, Joost-Pieter , Publisher =. Principles of model checking , Year =

    work page

  37. [37]

    2009 , publisher=

    Verification and Control of Hybrid Systems: A Symbolic Approach , author=. 2009 , publisher=

    work page 2009

  38. [38]

    Computer Aided Verification: 9th International Conference, CAV'97 Haifa, Israel, June 22--25, 1997 Proceedings 9 , pages=

    HyTech: A model checker for hybrid systems , author=. Computer Aided Verification: 9th International Conference, CAV'97 Haifa, Israel, June 22--25, 1997 Proceedings 9 , pages=. 1997 , organization=

    work page 1997

  39. [39]

    IEEE Transactions on Automatic Control , volume=

    Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems , author=. IEEE Transactions on Automatic Control , volume=. 2015 , publisher=

    work page 2015

  40. [40]

    2004 , publisher=

    Convex optimization , author=. 2004 , publisher=

    work page 2004

  41. [41]

    Convex programs for temporal verification of nonlinear dynamical systems , pages =

    Prajna, Stephen and Rantzer, Anders , year =. Convex programs for temporal verification of nonlinear dynamical systems , pages =

    work page

  42. [42]

    , Journal =

    Parrilo, Pablo A. , Journal =. Semidefinite programming relaxations for semialgebraic problems , Volume =

    work page

  43. [43]

    Proceedings of the 41st IEEE Conference on Decision and Control, 2002

    Introducing SOSTOOLS: A general purpose sum of squares programming solver , author=. Proceedings of the 41st IEEE Conference on Decision and Control, 2002. , pages=. 2002 , publisher =

    work page 2002

  44. [44]

    International Conference on Computer Aided Verification , pages=

    An antichain algorithm for LTL realizability , author=. International Conference on Computer Aided Verification , pages=. 2009 , publisher =

    work page 2009

  45. [45]

    Formal Methods in System Design , volume=

    Antichains and compositional algorithms for LTL synthesis , author=. Formal Methods in System Design , volume=. 2011 , publisher=

    work page 2011

  46. [46]

    IEEE Transactions on Automatic Control , volume=

    From small-gain theory to compositional construction of barrier certificates for large-scale stochastic systems , author=. IEEE Transactions on Automatic Control , volume=. 2022 , publisher=

    work page 2022

  47. [47]

    On the complexity of -automata , author=. Proc. 29th IEEE Symp. Found. of Comp. Sci , pages=. 1988 , publisher =

    work page 1988

  48. [48]

    2021 60th IEEE Conference on Decision and Control (CDC) , pages=

    Safety verification of dynamical systems via k-inductive barrier certificates , author=. 2021 60th IEEE Conference on Decision and Control (CDC) , pages=. 2021 , organization=

    work page 2021

  49. [49]

    Information and computation , volume=

    Reasoning about infinite computations , author=. Information and computation , volume=. 1994 , publisher=

    work page 1994

  50. [50]

    International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    Z3: An efficient SMT solver , author=. International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    work page

  51. [51]

    Satisfiability modulo Theories: Introduction and Applications , year =

    De Moura, Leonardo and Bj. Satisfiability modulo Theories: Introduction and Applications , year =. Commun. ACM , pages =

    work page

  52. [52]

    , year =

    Gao, Sicun and Kong, Soonho and Clarke, Edmund M. , year =. Automated

    work page

  53. [53]

    , year =

    Gao, Sicun and Avigad, Jeremy and Clarke, Edmund M. , year =. -. Automated

    work page

  54. [54]

    International Conference on Computer Aided Verification , pages=

    A fast linear-arithmetic solver for DPLL (T) , author=. International Conference on Computer Aided Verification , pages=. 2006 , publisher =

    work page 2006

  55. [55]

    2006 , publisher=

    Theory of computation , author=. 2006 , publisher=

    work page 2006

  56. [56]

    International Conference on Computer Aided Verification , pages=

    From LTL to deterministic automata: A safraless compositional approach , author=. International Conference on Computer Aided Verification , pages=. 2014 , organization=

    work page 2014

  57. [57]

    Formal methods in system design , volume=

    Model checking of safety properties , author=. Formal methods in system design , volume=. 2001 , publisher=

    work page 2001

  58. [58]

    International Conference on Computer Aided Verification , pages=

    Acacia+, a tool for LTL synthesis , author=. International Conference on Computer Aided Verification , pages=. 2012 , publisher=

    work page 2012

  59. [59]

    IEEE Transactions on Automatic Control , pages=

    Control barrier function based quadratic programs for safety critical systems , author=. IEEE Transactions on Automatic Control , pages=. 2016 , publisher=

    work page 2016

  60. [60]

    Automatica , pages=

    Control barrier functions for stochastic systems , author=. Automatica , pages=. 2021 , publisher=

    work page 2021

  61. [61]

    18th Annual Symposium on Foundations of Computer Science , pages=

    The temporal logic of programs , author=. 18th Annual Symposium on Foundations of Computer Science , pages=. 1977 , organization=

    work page 1977

  62. [62]

    2014 International Conference on Embedded Software (EMSOFT) , pages=

    Deductive control synthesis for alternating-time logics , author=. 2014 International Conference on Embedded Software (EMSOFT) , pages=. 2014 , organization=

    work page 2014

  63. [63]

    2016 IEEE 55th Conference on Decision and Control , pages=

    Automata theory meets approximate dynamic programming: Optimal control with temporal logic constraints , author=. 2016 IEEE 55th Conference on Decision and Control , pages=. 2016 , organization=

    work page 2016

  64. [64]

    2020 59th IEEE Conference on Decision and Control , pages=

    BP-RRT: Barrier pair synthesis for temporal logic motion planning , author=. 2020 59th IEEE Conference on Decision and Control , pages=. 2020 , organization=

    work page 2020

  65. [65]

    25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    k-Inductive Barrier Certificates for Stochastic Systems , author=. 25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    work page

  66. [66]

    International symposium on automated technology for verification and analysis , pages=

    Bounded synthesis , author=. International symposium on automated technology for verification and analysis , pages=. 2007 , publisher=

    work page 2007

  67. [67]

    2011 , publisher=

    Bradley, Aaron R , booktitle=. 2011 , publisher=

    work page 2011

  68. [68]

    International Workshop on Hybrid Systems: Computation and Control , pages=

    Model checking of hybrid systems: From reachability towards stability , author=. International Workshop on Hybrid Systems: Computation and Control , pages=. 2006 , organization=

    work page 2006

  69. [69]

    Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004

    Transition invariants , author=. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004. , pages=. 2004 , organization=

    work page 2004

  70. [70]

    International Conference on Computer Aided Verification , pages=

    Relational abstractions for continuous and hybrid systems , author=. International Conference on Computer Aided Verification , pages=. 2011 , publisher=

    work page 2011

  71. [71]

    de Moura, Leonardo and Rueß, Harald and Sorea, Maria , year =. Bounded. Computer

    work page

  72. [72]

    Bak, Stanley , year =. t-. 6th

    work page

  73. [73]

    IEEE Transactions on Automatic Control , volume=

    Symbolic control of stochastic systems via approximately bisimilar finite abstractions , author=. IEEE Transactions on Automatic Control , volume=. 2014 , publisher=

    work page 2014

  74. [74]

    Formal Methods in System Design , volume=

    Constructing invariants for hybrid systems , author=. Formal Methods in System Design , volume=. 2008 , publisher=

    work page 2008

  75. [75]

    Non-linear loop invariant generation using Gr

    Sankaranarayanan, Sriram and Sipma, Henny B and Manna, Zohar , booktitle=. Non-linear loop invariant generation using Gr

    work page

  76. [76]

    IEEE Control Systems Letters , volume=

    Koopman-inspired implicit backward reachable sets for unknown nonlinear systems , author=. IEEE Control Systems Letters , volume=. 2023 , publisher=

    work page 2023

  77. [77]

    Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) , pages=

    Multi-layered abstraction-based controller synthesis for continuous-time systems , author=. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) , pages=

    work page

  78. [78]

    Symbolic controller synthesis for B

    Majumdar, Rupak and Mallik, Kaushik and Soudjani, Sadegh , booktitle=. Symbolic controller synthesis for B

    work page

  79. [79]

    IEEE Robotics and Automation Letters , volume=

    Planning with learned dynamics: Probabilistic guarantees on safety and reachability via lipschitz constants , author=. IEEE Robotics and Automation Letters , volume=. 2021 , publisher=

    work page 2021

  80. [80]

    Numerically-

    Gao, Sicun and Kapinski, James and Deshmukh, Jyotirmoy and Roohi, Nima and Solar-Lezama, Armando and Arechiga, Nikos and Kong, Soonho , editor =. Numerically-. 2019 , pages =. doi:10.1007/978-3-030-25543-5_9 , booktitle =

    work page doi:10.1007/978-3-030-25543-5_9 2019

Showing first 80 references.