Pith. sign in

REVIEW 5 major objections 4 minor 27 references

Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains

T0 review · 5 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read This paper claims that hybrid automata can be translated into frequency automata that simulate by rotating vectors on the unit circle, making every level crossing exact and cutting simulation steps by factors of 118 to 1129.

desk verdict A trigonometric reparameterization of a narrow class of hybrid automata, with a circular soundness proof and benchmarks outside the stated guard class, but a real kernel of an idea for precise event detection. read the letter →

arxiv 2506.00251 v1 pith:NFV6IRCU submitted 2025-05-30 cs.FL

Moon Kim , Avinash Malik , Partha Roop This is my paper
classification cs.FL
keywords frequencyautomatahybridlevelcrossingdetectionunitcircleangularvelocitysoundtranslationsimulationnon-standardanalysis
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper introduces frequency automata, a formal model in which each continuous state variable of a hybrid automaton becomes a vector rotating on the unit circle, so a location's dynamics are given by an angular velocity rather than an ordinary differential equation. The authors claim a sound translation from hybrid automata to frequency automata: every execution trace of the original automaton has a matching trace in the frequency model, with mode switches occurring at the same times and with the same variable values. Because a guard condition becomes a target angle on the unit circle, the simulator can compute a step that lands exactly on the crossing instead of searching for it, which the authors argue makes level-crossing detection precise for the first time. On three published benchmarks, the frequency-automata simulator detects crossings that Matlab Simulink/Stateflow misses, including an equality guard, and runs 118x to 1129x faster while matching or exceeding a high-resolution reference trace. If the claims hold, hybrid-system simulation no longer needs dense time-stepping near guards.

What carries the argument

The load-bearing object is the unit-circle projection of each normalized state variable, defined by $x^n_f(t)=\sin(\theta(t))$, with angular velocity $\dot\theta(t)=\dot x^n_f(t)/\cos(\theta(t))$ derived from the increment theorem of non-standard analysis. This identity lets the translator turn a guard $x\bowtie q$ into a target angle $\theta(T)=\arcsin(x^n_f(T))$, and Lemma 4.3 guarantees that the remaining angle $\Delta\theta=\theta(T)-\theta(t)$ can be converted into a time step $\Delta t$ that lands exactly on the crossing. The simulation algorithm caps the angle step, computes the corresponding time step, and halves it until a user-set error bound is met, while never overshooting the guard angle. The mechanism's power is that the step size is driven by distance to the guard in angle space rather than by a fixed time grid, so the crossing is approached in a handful of rotations.

What would settle it

Take a one-location hybrid automaton with $\dot x=(x-a)(b-x)$, initial $x_0<a$, and guard $x=b$. The derivative changes sign before the guard, so the angular velocity changes sign; run the FA translation and check whether the simulator still hits $x=b$ exactly. If it misses, takes a negative time step, or requires range information that was not supplied statically, the convergence lemma does not hold outside the constant-sign case.

Watch

Extended reading notes

Core claim

The central claim is that the semantics of a hybrid automaton can be reproduced exactly by a frequency automaton, in which every continuous variable $x(t)$ is normalized to $x^n_f(t)=(x(t)-x_0)/\mathrm{range}(x)$ and identified with $\sin(\theta(t))$ for a vector rotating on the unit circle. The rate of change of the normalized variable becomes the angular velocity $\dot\theta(t)=\dot x^n_f(t)/\cos(\theta(t))$, and the value that triggers an outgoing guard becomes an angle $\theta(T)=\arcsin(x^n_f(T))$. With that angle in hand, the simulation takes a step $\Delta\theta$ chosen so that $\int_t^{t+\Delta t}\dot x\,d\tau$ exactly satisfies the guard; the paper's Lemma 4.3 shows such a step always exists within one revolution and that the resulting stop times match those of the original hybrid automaton, giving trace equivalence (Theorem 4.1). The authors present this as the first precise detection of every level crossing of a hybrid automaton, and report that on their benchmarks the simulator takes tens to hundreds of steps where a commercial tool needs thousands to tens of thousands.

Load-bearing premise

The translation is built on knowing, before execution, the maximum range of every state variable in every location and on a constant sign of the angular velocity toward the guard, because without that range the normalization and the guard angle cannot be constructed.

Editorial extensions

If this is right

  • A hybrid automaton satisfying the paper's assumptions can be simulated without ever missing a guard crossing, even when the guard is an equality such as $x=100$.
  • The number of simulation steps is set by angular increments rather than by a time-domain step size, so simulations with coarse angle steps still land exactly on crossings while remaining accurate.
  • Because the translation is claimed to be sound, any tool that can execute a frequency automaton inherits behavior equivalent to the original hybrid automaton, preserving stop times and variable values.
  • The reported speedups (118x to 1129x) come from replacing dense time-stepping with few, guard-directed steps, which would make long-horizon hybrid-system simulation practical.
  • Level-crossing detection with complex guards, including equality, becomes possible in a formal automaton model rather than requiring solver-specific heuristics.

Reading between the lines

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

  • Beyond the paper, the same unit-circle machinery could be applied to verification: if a frequency automaton trace runs in angle space, temporal-logic properties over guard-crossing times might be checked by symbolic angle arithmetic rather than by dense sampling.
  • The paper's benchmarks all have single-variable guards of the form $x\bowtie q$; extending the guard-angle construction to conjunctions, disjunctions, and nonlinear functions of several variables would be a testable next step the paper does not undertake.
  • The static range assumption suggests a natural stress test: run the translation on a system whose range is not known in advance, or whose derivative changes sign before the guard, and measure whether the claimed exact detection still holds.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 4 minor

Summary. The paper introduces Frequency Automata (FA), a proposed formal model of hybrid systems in which each continuous variable is normalized by a statically known range and represented by the sine of a phase angle on the unit circle. The ODE is replaced by an angular velocity, simulation advances in angular steps, and the step size is chosen to land exactly on a guard angle. The authors claim a sound translation from Hybrid Automata (HA) to FA, precise level-crossing detection, and 118x to 1129x speedups over Simulink/Stateflow, supported by three benchmarks: a steering wheel, a robot control example, and a water heating system.

Significance. The angle-stepping idea is interesting and, for monotone flows with known bounds, may detect level crossings more reliably than fixed-step time integration; the steering-wheel example illustrates this potential. The paper deserves credit for presenting formal definitions, a proof skeleton, and an empirical comparison with an industry tool. However, the central formal claim is not established: the translation is defined only under a static-range assumption that the HA syntax does not guarantee, the equivalence proof is largely a restatement of the change of variables defining the FA, and the experiments use guards outside the formal guard class. If these issues were repaired, the contribution would be a restricted simulation technique rather than the general sound translation and first precise level-crossing result claimed in the paper.

major comments (5)
  1. [Section 2.1, Assumption 3; Definition 12] The normalization x_n_f(l,x_f(t)) = (x_f(t)-x_f(0))/max(range(l,x_f(t))) requires max(range(...)) to be finite and statically known, but Definitions 9 and 10 do not guarantee this. A well-formed HA can have a location with invariant true, x_dot = 1, and an outgoing guard on a different variable that never fires; x is then unbounded while the location is occupied, so max(range) = infinity and the FA normalization is undefined. Even when the range is finite, as in the robot benchmark, it depends on the first hitting time of a nonlinear guard and cannot be derived from the syntax of Definition 10. The claim in Section 4 that ranges are known statically 'because of Definition 10' is therefore incorrect, and Theorem 4.1 is not a theorem about the HA class of Definitions 9-10.
  2. [Definition 10; Section 6 benchmarks] The formal guard class is g := x ⊲⊳ Q with ⊲⊳ in {≥, ≤}, a single-variable inequality. The robot benchmark uses y ≥ 12x^2 - 54x + 65, which is a multi-variable nonlinear guard, and the water-heating benchmark uses temp == 100, an equality guard. Both are outside Definition 10, yet the experiments in Section 6 and the claims about 'complex guards (including equality)' are presented as validating the formal framework. The paper therefore does not demonstrate the sound translation or the precise level-crossing result for the benchmark class it actually evaluates.
  3. [Lemma 4.2; Theorem 4.1] Lemma 4.2 assumes Δx_n_f = Δsin and derives x_n_f(t) = sin(θ_x(t)), but the FA construction in Definition 12 and Section 2.1 defines the normalized variable through this sine projection and then sets the angular velocity to x_dot_n/cos(θ). Equation (1) is thus the defining identity of the construction, not a derived equivalence. The proof of Theorem 4.1 uses Lemma 4.2 to conclude that x(t) = x_f(t), so the claimed soundness of the translation holds by construction rather than as a substantive trace-equivalence result for arbitrary HAs in the stated class.
  4. [Lemma 4.3; Definition 13; Algorithm 2] Lemma 4.3 assumes that 'the ODEs in the location evolve the HA towards one of its outgoing guards' for the whole interval, and Definitions 11 and 13 build the same monotone-approach requirement into the definition of stop times. The proof then selects the clockwise or counterclockwise angle based on the sign of θ_dot. Consequently, the convergence result covers only trajectories with constant-sign approach to the guard, not all well-formed HAs. In Algorithm 2, line 5 computes Δt = Δθ cos(θ_x(T))/x_dot_n(T) with no check for x_dot_n(T) = 0 or cos(θ_x(T)) = 0, and it can return a negative time step when the two factors have opposite signs. The halving loop condition abs(x_fc - x'_fc) ≤ ε_u is also the reverse of the usual error criterion, since it continues halving while the difference is already small and stops when the difference is large. These issues undercut the claim that the algorithm 'is guaranteed to converge to the level crossing without missing it.'
  5. [Section 6, Table 1 and Figure 7; Section 4 running example] Table 1 reports for the robot benchmark that Simulink/Stateflow with max step 0.01 achieves accuracy >0.99999999 with 706 steps, whereas Section 6 and Figure 7 state that Simulink with max step 0.01 fails to detect the guard and continues through the obstacle; these two descriptions are inconsistent. For water heating at error tolerance 1e-6, FA (π/10) takes 7802 steps (0.785956 s) versus Simulink(0.001) at 20006 steps (1.023724 s), only about 1.3x faster, so the abstract's '118x to 1129x' range selects only the most favorable configurations. In the steering-wheel FA translation in Section 4, X_n_f is written with denominator 0.99 for x_n, while the accompanying text says max(range(x)) = max([π/2, abs(arccos(−0.99))]) ≈ 3.0; with 0.99, the guard angle arcsin(1.44) is undefined, making the formalized running example internally inconsistent.
minor comments (4)
  1. [Lemma 4.2 heading] The heading contains a typo: 'Eqivalence relation' should read 'Equivalence relation.'
  2. [Section 4, FA translation example] In the FA translation example, y_n_f is defined as y(t) - cos(π/2) without division by a range, which is inconsistent with the normalization formula in Definition 12.
  3. [Definition 9] The tuple in Definition 9 includes an update function h, but the semantics in Definition 11 and the subsequent translation never use h; this unused component should be removed or its role clarified.
  4. [Front matter and template] The manuscript still contains placeholder template material, including the CCS Concepts text 'Do Not Use This Code' and an ACM reference format with 2018 dates; these should be replaced before any resubmission.

Circularity Check

3 steps flagged · score 8.0 of 10

The paper's 'precise level crossing detection' is assumed as an input to the FA construction (Section 2.1 assumption 2); the FA guard angle is arcsin of the known crossing value, and Lemma 4.2 is a change of variables, so the central soundness claim reduces to its own assumptions by construction.

  1. fitted input called prediction [Section 2.1, assumptions (1)-(3); Definition 12 example (FA syntax)]
    "The (possibly symbolic) value of the state variable(s) that trigger one or more outgoing edge(s) from a given location. For the steering wheel example, we know that 𝑥(𝑇) = arccos(−0.99) triggers the outgoing edge guard from location 𝐿1 at some time 𝑇."

    This assumed value is exactly the level crossing whose 'precise detection' is advertised as the paper's main contribution (Abstract; Section 1, contribution 3). The FA guard angle is then constructed from this input in Definition 12's example: 𝐺𝑓(𝐿1,𝐿2,...) = [arcsin((arccos(−0.99)−𝜋/2)/max(𝑟𝑎𝑛𝑔𝑒(𝑥𝑓(𝑡))))]. The FA does not discover the crossing; the guard-satisfying value that the HA execution would produce is installed in the automaton at construction time. The claimed 'detection' is the input, renamed as a predicted result.

  2. renaming known result [Section 2.1 Step-(4) and Step-(5); Lemma 4.2; Definition 12 (Ω𝑓)]
    "Hence, Δ𝑥𝑛 = Δ sin = sin(𝜃𝑥+ Δ𝜃𝑥)− sin(𝜃𝑥), where Δ𝜃𝑥 =𝜃𝑥(𝑡+ Δ𝑡)−𝜃𝑥(𝑡)."

    Step-(4) defines Δ sin to equal Δ𝑥𝑛, and Lemma 4.2 then 'derives' 𝑥𝑛𝑓(𝑡)=sin(𝜃𝑥(𝑡)) from that equality by integration. But this equality is just the definition of the angle 𝜃𝑥(𝑡)=arcsin(𝑥𝑛𝑓(𝑡)), and Definition 12 defines Ω𝑓 via 𝐷(𝑥𝑛𝑓(𝑡)) = 𝑥̇𝑛𝑓(𝑡)/cos(𝜃𝑥(𝑡)), which is exactly the derivative of arcsin. The 'frequency-domain representation' is therefore a change of variables of the same ODE, not a new model with independent dynamics. Theorem 4.1's equivalence reduces to this renaming; no behavioural content is added by Lemma 4.2 beyond the coordinate transformation.

1 more flagged steps
  1. self definitional [Lemma 4.3 (Convergence to the guard); Algorithm 2]
    "Consider, without loss of generality, some out going edge (𝑒) guard from location 𝑣(𝑡), such that 𝑥(𝑇𝑘+1) satisfies 𝐺(𝑒), where 𝑇𝑘+1 is the first time where the outgoing edge guard condition holds."

    The convergence lemma assumes the very fact that the FA is supposed to determine—the existence, value, and first time of the level crossing—and then uses that known crossing value to compute Δ𝑥, Δ𝑥𝑛𝑓, and Δ𝜃𝑥. Algorithm 2 likewise takes as input the 'angle of the guard' that was built from the assumed crossing value, so the step size is chosen to hit a pre-supplied target. Combined with the guard angles constructed in Definition 12, the 'guaranteed convergence to the level crossing' is true by construction, so Theorem 4.1 imports the crossing information rather than deriving it from the HA's dynamics.

full rationale

The central derivation chain is circular in a precise sense. The paper's advertised result—precise level-crossing detection (Abstract; Section 1 contribution 3)—is not derived from the FA execution but is supplied as input in Section 2.1 assumptions (1)-(3), including the exact variable value that triggers the guard. Definition 12 converts this assumed value into a guard angle via arcsin, and Algorithm 2 takes the 'angle of the guard' as input, so reaching that angle is guaranteed by construction. Lemma 4.2 asserts x_n = sin(θ) after defining Δ sin := Δx_n and θ̇ = ẋ_n/cos θ, which is a change of variables rather than a substantive equivalence. Lemma 4.3 assumes the guard time exists and then 'converges' to the precomputed target, so Theorem 4.1 is a trace-preservation statement for a repackaged ODE rather than a derivation of detection capability. This is not a self-citation issue: the authors' prior works [17] and [22] are cited for background but are not load-bearing for the translation theorem. The benchmark comparison against Simulink/Stateflow is genuine external evidence for speed, but it does not rescue the circularity of the theoretical 'first precise detection' claim. The empirical speedup claim alone might merit a low score, but because the paper's headline theoretical contribution reduces to its own input, the circularity score is 8.

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

The paper introduces no new physical entities; the 'frequency automaton' is a formal tuple whose content reduces to the substitution x_n=sin(theta). The central derivation depends on statically known ranges and user-chosen step and error parameters, listed above.

free parameters (3)
  • max(range(l, x_f(t))) for each location-variable = steering wheel: 0.99; robot and water heating values not stated in the paper
    Used to normalize x_n=(x_f-x0)/range and to define the guard angle on the unit circle; assumed known statically, but for general ODEs it is not computable without solving the system.
  • maximum angle increment Delta_theta_u = pi/10, pi/50, pi/100, pi/150 across benchmarks
    User-supplied cap on the angular step in Algorithm 2; determines step count and reported speedup.
  • error tolerance epsilon_u = 1e-6, 1e-4, 1e-2 across benchmarks
    Step-halving termination criterion in Algorithm 2; the claimed precision is relative to this hand-set bound.
assumptions (6)
  • domain assumption HA flows are restricted to x_dot(t)=f(x(t)) in each location.
    Stated in Section 1.2 and Definition 9; excludes time-dependent and higher-order ODEs.
  • domain assumption The HA subset has switching behaviour only: the intersection of any guard with the corresponding invariant is empty.
    Stated in Section 1.2; excludes Zeno and continuous-urgent behaviours.
  • ad hoc to paper The maximum range of every state variable in every location is known statically before execution.
    Section 2.1 assumptions (1)-(3); needed for normalization and guard angles; not generally obtainable.
  • domain assumption Guards are restricted to single-variable comparisons x triangleq Q.
    Definition 10; the robot benchmark uses y >= 12x^2 - 54x + 65 and the water heating benchmark uses temp == 100, which are outside this class.
  • ad hoc to paper The flow evolves monotonically toward the outgoing guard, so angular velocity has a constant sign inside a location.
    Lemma 4.3 assumes the ODEs evolve toward the guard and selects the nearest angle in the current direction; oscillations or turning points are not handled.
  • standard math Non-standard analysis machinery: transfer principle, standard part, increment theorem.
    Section 3; used only to write derivatives, and the final derivation does not depend on hyperreal details.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains." pith.science (2026). https://pith.science/paper/NFV6IRCU

@misc{pith2026250600251,
  author       = {Pith},
  title        = {Pith review of: Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NFV6IRCU}},
  note         = {Machine review of arXiv:2506.00251}
}
read the original abstract

Hybrid systems are mostly modelled, simulated, and verified in the time domain by computer scientists. Engineers, however, use both frequency and time domain modelling due to their distinct advantages. For example, frequency domain modelling is better suited for control systems, using features such as spectra of the signal. Considering this, we introduce, for the first time, a formal model called frequency automata for hybrid systems modelling and simulation, which are represented in combined time and frequency domains. We propose a sound translation from Hybrid Automata (HA) to Frequency Automata (FA). We also develop a numerical simulator for FA and compare it with the performance of HA. Our approach provides precise level crossing detection and efficient simulation of hybrid systems. We provide empirical results comparing simulation of HA via its translation to FA and its simulation via Matlab Simulink/Stateflow. The results show clear superiority of the proposed technique with the execution times of the proposed technique 118x to 1129x faster compared to Simulink/Stateflow. Moreover, we also observe that the proposed technique is able to detect level crossing with complex guards (including equality), which Simulink/Stateflow fail.

Figures

Figures reproduced from arXiv: 2506.00251 by the authors.

Figure 1
Figure 1. Steering wheel of a car and its implementation in Stateflow [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Outputs from the Stateflow model for a 50 sec simulation time [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. HA representation of the steering wheel system [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Translating cartresian coordinates to polar coordinates during translation of HA to FA [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: Level crossings and current vector position [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 6
Figure 6. Figure 6: Comparison of Simulink and FA step sizes and precision. Y-axis in all plots shows cos(𝑥 (𝑡) ) for the steering wheel benchmark. Figure 6f shows the simulation results of FA with the maximum angle increment bounded to 𝜋/100. It shows that the level crossing is correctly…
Figure 7
Figure 7. Figure 7: Simulation of the second benchmark — Robot Control [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: shows the simulation results of the third benchmark, water heating system. The guard predicate to detect the water temperature reaching 100 degrees should be 𝑡𝑒𝑚𝑝(𝑡) == 100. However, Simulink/Stateflow® cannot handle equality in guard conditions even with a very fine t…
Figure 9
Figure 9. Figure 9: Accuracy vs. Number of Steps between FA and Simulink/Stateflow® [PITH_FULL_IMAGE:figures/full_fig_p018_9.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

27 extracted references · 26 canonical work pages

  1. [1]

    Matthias Althoff and Bruce H Krogh. 2014. Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Automat. Control 59, 2 (2014), 371–383

    work page 2014

  2. [2]

    Rajeev Alur. 2015. Principles of Cyber-Physical Systems . MIT Press

    work page 2015

  3. [3]

    Rajeev Alur and David L Dill. 1994. A theory of timed automata. Theoretical computer science 126, 2 (1994), 183–235

    work page 1994

  4. [4]

    Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking . MIT press. 19 Conference acronym ’XX, June 03–05, 2018, Woodstock, NY Kim et al

    work page 2008

  5. [5]

    Niraj Basnet and Houssam Abbas. 2020. Logical signal processing: A fourier analysis of temporal logic. In Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings 20 . Springer, 359–382

    work page 2020

  6. [6]

    Benveniste, P

    A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1 (Jan. 2003), 64–83. https://doi.org/10.1109/JPROC.2002.805826

    work page arXiv 2003

  7. [7]

    Luca Benvenuti, Davide Bresolin, Pieter Collins, Alberto Ferrari, Luca Geretti, and Tiziano Villa. 2014. Assume– guarantee verification of nonlinear hybrid systems with Ariadne. International Journal of Robust and Nonlinear Control 24, 4 (2014), 699–724

    work page 2014

  8. [8]

    Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification . Springer, 258–263

    work page 2013

Show all 27 references
  1. [9]

    Suresh R Devasahayam. 2019. Signals and systems in biomedical engineering: physiological systems modeling and signal processing. Springer

    2019

  2. [10]

    Alexandre Donzé. 2013. On signal temporal logic. In Runtime Verification: 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings 4 . Springer, 382–383

    2013

  3. [11]

    Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, and Scott Smolka. 2012. On temporal logic and signal processing. In Automated Technology for Verification and Analysis: 10th International Symposium, ATV A 2012, Thiruvananthapuram, India, October 3-6, 201...

    2012

  4. [12]

    Joel M Esposito, Vijay Kumar, and George J Pappas. 2001. Accurate event detection for simulating hybrid systems. In International Workshop on Hybrid Systems: Computation and Control . Springer, 204–217

    2001

  5. [13]

    Joaquín Fernández and Ernesto Kofman. 2014. A stand-alone quantized state system solver for continuous system simulation. Simulation 90, 7 (2014), 782–799

    2014

  6. [14]

    Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In Proceedings of the 23rd International Conference on Computer Aid...

    2011

  7. [15]

    H Jerome Keisler. 2013. Elementary calculus: An infinitesimal approach . Courier Corporation

    2013

  8. [16]

    Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems . Springer, 152–166

    2004

  9. [17]

    Avinash Malik and Partha Roop. 2020. A dynamic quantized state system execution framework for hybrid automata. Nonlinear Analysis: Hybrid Systems 36 (2020), 100870

    2020

  10. [18]

    Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V Deshmukh, Ken Butts, and Taylor T Johnson. 2017. Abnormal data classification using time-frequency temporal logic. In Proceedings of the 20th international conference on hybrid systems: Computation and control . 237–242

    2017

  11. [19]

    Taeshin Park and Paul I Barton. 1996. State event location in differential-algebraic models. ACM Transactions on Modeling and Computer Simulation (TOMACS) 6, 2 (1996), 137–165

    1996

  12. [20]

    Amir Pnueli. 1977. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977). ieee, 46–57

    1977

  13. [21]

    Jean-François Raskin. 2005. An introduction to hybrid automata. In Handbook of networked and embedded control systems. Springer, 491–517

    2005

  14. [22]

    Jin Woo Ro, Avinash Malik, and Partha Roop. 2019. A compositional semantics of simulink/stateflow based on quantized state hybrid automata. In Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. 1–11

    2019

  15. [23]

    Alena Rodionova, Ezio Bartocci, Dejan Nickovic, and Radu Grosu. 2016. Temporal logic as filtering. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control . 11–20

    2016

  16. [24]

    Sucheta Sehgal, Nitish D Patel, Avinash Malik, Partha S Roop, and Mark L Trew. 2019. Resonant model—A new paradigm for modeling an action potential of biological cells. PLoS One 14, 5 (2019), e0216999

    2019

  17. [25]

    Han Su, Saumya Shankar, Srinivas Pinisetty, Partha S Roop, and Naijun Zhan. 2025. Runtime Enforcement of CPS against Signal Temporal Logic. arXiv preprint arXiv:2502.11584 (2025)

    2025 arXiv

  18. [26]

    Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. 2009. Formal methods: Practice and experience. ACM computing surveys (CSUR) 41, 4 (2009), 1–36

    2009

  19. [27]

    Fu Zhang, Murali Yeddanapudi, and Pieter J Mosterman. 2008. Zero-crossing location and detection algorithms for hybrid system simulation. IFAC Proceedings Volumes 41, 2 (2008), 7967–7972. Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009 20

    2008

Pith tools

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