Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

Falsification of Autonomous Systems in Rich Environments

T0 review · 3 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read This paper claims that falsifying a black-box autonomous system—finding an environment in which its neural-network controller violates a formal specification—can be reformulated as a motion-planning problem for a "meta-system," solved by…

desk verdict A genuinely useful reformulation of black-box falsification as planning in the meta-state space, with a real efficiency demonstration in one scenario, but the headline claim is scoped too broadly and the pseudocode has reproduction bugs. read the letter →

arxiv 2412.17992 v1 pith:PYMYAZD7 submitted 2024-12-23 cs.RO cs.SYeess.SY

Khen Elimelech , Morteza Lahijanian , Lydia E. Kavraki , Moshe Y. Vardi This is my paper · ORCID
classification cs.ROcs.SYeess.SY
keywords falsificationblack-boxtestingcyber-physicalsystemsneuralnetworkcontrollerssampling-basedmotionplanningRRTmeta-planningincrementalsimulation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper's aim is to make black-box falsification of autonomous systems cheaper: find an environment that makes a neural-network-controlled agent violate its formal specification while spending as few controller queries (simulation steps) as possible. Its central proposal is to stop sampling environments independently and instead treat the search as a motion-planning problem in a "meta-state space," where each state bundles an environment together with the full simulated trajectory and sensor history it produces. A mutation of the environment is a meta-control, and the falsifying condition is a goal region, so any forward-search sampling-based planner (RRT is demonstrated) can grow a tree of tests. The decisive efficiency mechanism is incremental simulation: because the environment is only partially observable from the agent's sensors, a local change to an environment element invalidates only the suffix of the previous trajectory after the change was first observed, so each new test reuses the prefix and simulates only the remainder. If correct, the approach would let a tester with no access to the controller or dynamics—and optionally no domain knowledge at all—falsify well-trained controllers with roughly 40–60% fewer simulation steps than random, genetic, or Bayesian-optimization baselines, in the demonstrated obstacle-avoidance scenario.

What carries the argument

The load-bearing construction is the meta-state space S: each meta-state s = (env, ξ, z) is a valid simulated scene in which the system trajectory ξ and observation history z are generated by running the black-box controller and sensor model in environment env. The meta-dynamics F(s, mut) = s' applies a mutation mut to the environment's element collection and updates the trajectory incrementally: it finds the first timestamp T at which the observation in the mutated environment differs from the stored history (the "history-compromise timestamp"), reuses the trajectory prefix up to T, and simulates only the suffix from state ξ_T in the mutated environment. This prefix-reuse identity is what converts serial independent tests into a search tree in which each new environment costs only the simulation of the portion of the run affected by the change. The paper shows how to compute T domain-independently by regenerating observations at each stored state, or cheaply by geometric overlap checks when the sensor model is known, and it frames node selection through a composite meta-state distance (weighted environment distance plus trajectory distance) that lets RRT-style planners explore the space.

What would settle it

Run the same algorithm on an environment type where the mutated elements are observable from the system's initial state (for example, a track that is fully visible at time zero, or a mutation operator that changes global parameters such as track curvature rather than local elements), count neural-network controller calls per falsifying example, and compare with uniform random sampling. The paper's mechanism predicts that prefix reuse vanishes—each mutation forces a full re-simulation—so controller-call counts should approach or exceed those of independent sampling plus tree overhead; observing no such gap in this setting would put the central efficiency claim in doubt.

Watch

Extended reading notes

Core claim

The paper's core discovery is a reformulation: the falsification problem for an autonomous system under a formal specification is equivalent to a motion-planning problem for an under-actuated, discrete, Markovian meta-system that wraps the examined system. A meta-state is a valid simulated scene—a triple of environment, system trajectory, and observation history—and a meta-control is an environment mutation restricted to the element collections of the environment (local, optional, additive features such as obstacles, as opposed to global parameters such as track shape). The goal region is the set of meta-states whose status predicate reports specification failure, a purely Boolean predicate that abstracts away the specification's logic and therefore needs no robustness function and can express liveness as well as safety properties. Starting from one simulated scene, the planner grows a tree by mutating elements and re-simulating; because elements are only locally observable, the mutation compromises the observation history only from the first timestamp at which it is seen, so each extension is an incremental partial simulation rather than a fresh run. The paper claims this reformulation is not a new search algorithm but a new way of posing the problem that off-the-shelf sampling-based planners can solve, that it makes minimal assumptions (black-box controller, no dynamics model, no predefined input dimensionality), and that in the experimental obstacle-avoiding car scenario every one of its five variants outperformed uniform sampling, a genetic algorithm, and Bayesian optimization in controller calls—the best variant (RRT with a trajectory-distance metric) using 4524 control loops and 88.75 environments on average versus 11564 and 182.05 for uniform sampling.

Load-bearing premise

The efficiency gain relies on the environment being only partially observable by the system, so that a mutation of an environment element leaves the previously computed trajectory valid up to the moment the change is first observed; if a mutation is visible from the first timestep, or changes a global property such as an environment parameter, the entire trajectory prefix is invalid and each new test must be simulated from scratch, collapsing meta-planning's advantage.

Editorial extensions

If this is right

  • A tester who cannot define a robustness function—for example under non-quantitative, liveness, or PDDL-style specifications—can still falsify the system, because the goal region is just the Boolean status predicate rather than an optimization objective.
  • Because each tree extension reuses the trajectory prefix, the controller-call cost of evaluating a new environment is only a fraction of a full run; in the reported scenario the best variant used 4524 controller calls for 88.75 environments, whereas Bayesian optimization used 7901 calls for 123.14 environments.
  • Domain knowledge improves the search but is not required: even the no-domain-knowledge variant (random tree with unlimited mutation depth) used 62% of the uniform-sampling baseline's controller calls, and each additional comparative procedure (distance-to-failure heuristic, environment distance, trajectory distance) reduced the effort further.
  • The formulation is not tied to a specific planner, so any forward-search sampling-based planner—including future ones that exploit parallel simulation—inherits the incremental-simulation benefit without changing the problem statement.
  • Because the solution is the goal meta-state and not the path, the input dimension need not be fixed in advance, allowing open environments with variable numbers of elements to be falsified directly.

Reading between the lines

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

  • The parameter-versus-element split predicts a testable boundary for the method's value: when the failure-relevant environment is fully visible from the initial state, prefix reuse fails at timestamp zero and meta-planning should degenerate to independent sampling plus tree overhead; an experiment varying sensor range or observability would confirm or refute this prediction.
  • A direct extension the authors do not explore is prefix-sharing across multiple search trees or restarts, since validated trajectory prefixes are stored in each meta-state; a multi-root planner could reuse them and compound the savings demonstrated within a single tree.
  • The same wrapper applies to any black-box whose inputs are structured as collections of locally influential elements, not just sensor-driven robots—for instance, stress-testing learned policies in other expensive simulators by mutating local context items while keeping global settings fixed.
  • The distance-to-failure heuristic is just a scalar scoring of a completed run, so mature quantitative measures such as STL robustness could be plugged in as the node-selection heuristic without altering the incremental-simulation mechanism; conversely, the formulation works for specifications that have no quantitative semantics at all.
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

3 major / 5 minor

Summary. The paper proposes an environment-based testing model for black-box falsification of autonomous systems, then reformulates falsification as motion planning in a "meta-state" space whose states are (environment, system trajectory, observation history) triples. Meta-controls are environment mutations followed by simulation, and the paper instantiates the idea with RRT-style forward search, goal-biasing heuristics, and incremental simulation. The approach is evaluated on a lidar-equipped obstacle-avoiding car with a neural-network controller, comparing five meta-planning variants against random sampling, a genetic algorithm, and Bayesian optimization in terms of environments tested and controller calls.

Significance. If the claims hold, the meta-planning reformulation is a useful conceptual contribution: it connects falsification to sampling-based motion planning, supports general temporal specifications without requiring a robustness function, and can exploit incremental simulation to reduce per-test effort. The paper provides pseudocode, an open-source simulator, and a comparison against multiple baselines. However, the formal conditions under which incremental reuse is valid are not fully stated, and the experimental evidence is limited to a single scenario with no statistical significance testing, so the strength of the central efficiency claim is not yet established at the level claimed.

major comments (3)
  1. [Sec. 3.4, Eq. (7)] Eq. (7) and the surrounding text define T as the last timestamp at which h(xi_t, env) = h(xi_t, env') and assume the old trajectory prefix is valid up to T. However, the system model in Eq. (1) lets the environment-state appear in the vector field f, not only in the observation map h. If the mutation changes an element that affects dynamics before it is observed (e.g., an obstacle that causes contact before entering the sensor cone), the old prefix is not a valid trajectory in the mutated environment even though the observation histories coincide. The paper should either restrict mutations to elements that influence the system only through observations, or revise the incremental simulation to recompute from the first time f differs, and state this restriction wherever the per-test efficiency gain is claimed.
  2. [Secs. 2.1 and 3.4; Conclusion] The per-test efficiency claim is conditioned on local partial observability of every mutated element, but this precondition is not stated as a requirement. The environment formalism in Sec. 2.1 says elements "may be observed locally" rather than "must be observed locally," and the abstract and conclusion state the efficiency result without qualification. If an element is globally observable, find_history_compromise_timestamp returns 0 for every mutation, incremental simulation degenerates to full re-simulation, and the search tree only adds overhead over independent sampling. The authors should either define elements so that local observability is part of the definition, or explicitly list the partial-observability precondition as a scope condition on the main efficiency claim.
  3. [Sec. 5.2-5.3, Table 1] The claim that meta-planning "clearly" and "significantly" outperforms the baselines rests on a single scenario with 20 random seeds and no confidence intervals or hypothesis tests. In Table 1, the gap between the simplest meta-planning variant (7192 control loops) and Bayesian optimization (7901 control loops) is only about 9%, so without a statistical test the advantage for some variants is not established. Report per-seed distributions with confidence intervals and a test such as Mann-Whitney U or a bootstrap test, and preferably include at least one additional track shape, sensor configuration, or controller to support the generality of the conclusions.
minor comments (5)
  1. [Sec. 3.1] There is a duplicated phrase "the composite space of of inputs×outputs"; please proofread for similar typos elsewhere, e.g., "does not not require" in Sec. 4.5 and "to to 'hit'" in Appendix B.
  2. [Algorithm 2] In the simplified-distance branch of select_node, the last line references random_meta_state.env, but in that branch only random_env is defined; this appears to be a typo and should be corrected.
  3. [Eq. (10)] The trajectory distance in Eq. (10) parameterizes trajectories as functions y = f(x), which is not valid for trajectories with loops, vertical segments, or multiple y-values at the same x. A curve-distance based on Fréchet or Hausdorff distance would be more generally applicable.
  4. [Algorithm 3 and Sec. 4.4] The EXPANSION_BREADTH constant appears in Algorithm 3 but is not motivated or discussed in Sec. 4.4. A sentence describing its role and the value used in the experiments would improve reproducibility.
  5. [Sec. 5.2] The Bayesian-optimization baseline uses the distance-to-failure heuristic as the optimization objective rather than an actual robustness function; this is acknowledged in the text, but the results discussion should remind the reader that this makes the comparison to optimization-based robustness falsification indirect.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the meta-planning reformulation, the incremental-simulation mechanism, and the experimental comparison are all self-contained and do not reduce to their own inputs.

full rationale

The paper's central contribution is a reformulation of falsification as planning in a meta-state space, not a derivation that presupposes its conclusion. The meta-dynamics are defined (Eq. 6) and then specialized to incremental updates (Eq. 7) under an explicitly stated partial-observability assumption; the trajectory prefix is reused by construction, but this is an algorithmic identity rather than a circular prediction. The distance-to-failure heuristic, environment-distance function, and perturbation procedures are user-provided domain knowledge, not parameters fitted to the experimental outcome, and the experiments compare against independent baselines (random search, genetic algorithm, and Bayesian optimization) using the same heuristic where appropriate. The incremental-simulation benefit does depend on the environment being only partially observable, and the paper's abstract and conclusion state the efficiency result more broadly than that precondition; however, this is a scoping limitation, not a circular step, because the formalism itself defines elements as locally observable features. Self-citations, such as LiteRacer [68] and earlier planning-based falsification work by the same authors, are used as tools and background, not as load-bearing evidence for the novelty or correctness of the approach. No fitted parameter is renamed as a prediction, and no uniqueness theorem is imported from the authors' prior work to force the chosen formulation. The paper is therefore self-contained against the claims it actually demonstrates.

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

The central claim does not rest on a heavy axiom stack; it is an algorithmic reformulation. The efficiency advantage, however, rests on determinism plus partial observability, and the experimental numbers depend on several under-reported algorithm constants (EXPANSION_BREADTH, w in Eq. 8, goal-bias ratio, mutation depth). No invented entities are introduced.

free parameters (5)
  • goal_bias_ratio = 80% greedy / 20% exploration
    Set by experimenters in Sec. 5.2 for RRT variations; controls the balance between distance-to-failure guidance and random exploration, and affects all reported RRT results.
  • mutation_depth = Gaussian noise with std=(2,2)
    Used for meta-planning variations 2-5 and GA mutation (Sec. 5.2); chosen without sensitivity analysis, affects incremental-simulation reuse and search dynamics.
  • expansion_breadth = not reported
    Algorithm 3 loops over EXPANSION_BREADTH, but the value is never given in Sec. 5. Every meta-planning result depends on this per-expansion branching factor.
  • distance_weight_w = not reported
    Eq. (8) defines meta_state_distance as a convex combination of env distance and trajectory distance, but no w is reported for the unsimplified RRT experiments.
  • obstacle_configuration = 3 obstacles, radius 0.1
    The benchmark fixes three circular obstacles on a sinuous track; all effort numbers are specific to this configuration (Sec. 5.1).
assumptions (4)
  • domain assumption The system is deterministic: no actuation or sensing noise, and the environment-state is static during a run.
    Sec. 2.2 states this assumption; without it, the prefix-sharing incremental simulation in Sec. 3.4 would not preserve the validity of earlier observations.
  • domain assumption The environment is partially observable, so a mutation in environment elements does not alter the observation history before a timestamp T.
    Sec. 3.4 assumes 'the environment is only partially-observable by the system'; this is what allows trajectory prefixes to be reused across meta-states and drives the reported per-test savings.
  • standard math Sampling-based kinodynamic RRT retains probabilistic completeness under random forward extension.
    Sec. 4.4 cites LaValle and Kuffner [65] to justify that random meta-control extension does not sacrifice completeness; no proof is given for the meta-state space.
  • domain assumption The status predicate status(s) can be evaluated by a model checker for any scene.
    Sec. 2.3 assumes availability of a status predicate. In the example it is evaluated by geometric intersection checks, but no general checker is specified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Falsification of Autonomous Systems in Rich Environments." pith.science (2026). https://pith.science/paper/PYMYAZD7

@misc{pith2026241217992,
  author       = {Pith},
  title        = {Pith review of: Falsification of Autonomous Systems in Rich Environments},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PYMYAZD7}},
  note         = {Machine review of arXiv:2412.17992}
}
read the original abstract

Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of ``black-box testing'' rely on repeated system simulations to find a falsifying counterexample of a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort (NN inference queries) needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well-trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically-defined, open environments, which yield high-dimensional, simulation-dependent sensor observations. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for a ``meta-system,'' which wraps and encapsulates the examined system; we call this approach: meta-planning. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT) and can gradually integrate domain knowledge to improve the search. We support the suggested approach with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches.

Figures

Figures reproduced from arXiv: 2412.17992 by the authors.

Figure 1
Figure 1. Our running example: an autonomous car acting in an “obstructed track” environment, whose [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Testing models used for falsification of autonomous car system. [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. The meta-system model. , Vol. 1, No. 1, Article . Publication date: December 2024 [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Comparing the simulation of a scene (environment and initial state), and of the scene after locally [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: Solving the meta-planning problem: a forward search-tree, where meta-states (nodes) represent [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: “Box and whisker charts” representing the distribution of effort across trials. Lower is better. Each box [PITH_FULL_IMAGE:figures/full_fig_p022_6.png]
Figure 7
Figure 7. Figure 7: Illustration of the scene-sampling patterns of our incremental, tree-based, meta-planning sampler [PITH_FULL_IMAGE:figures/full_fig_p028_7.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Piecewise Control Barrier Functions for Stochastic Systems

    eess.SY 2025-07 conditional novelty 6.0 of 10

    The authors reformulate joint synthesis of a piecewise stochastic control barrier function and a safe controller as a single dual linear program claimed to have zero duality gap.

Reference graph

Works this paper leans on

71 extracted references · 71 canonical work pages · cited by 1 Pith paper

  1. [1]

    Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46–55 (Jun 2022)

    work page 2022

  2. [2]

    Singh, B., Kumar, R., Singh, V.P.: Reinforcement learning in robotic applications: A comprehensive survey. Artif. Intell. Rev. 55(2), 945–990 (Feb 2022)

    work page 2022

  3. [3]

    IEEE Transactions on Cybernetics pp

    Zare, M., Kebria, P.M., Khosravi, A., Nahavandi, S.: A Survey of Imitation Learning: Algorithms, Recent Developments, and Challenges. IEEE Transactions on Cybernetics pp. 1–14 (2024)

    work page 2024

  4. [4]

    Annual Review of Control, Robotics, and Autonomous Systems 1(Volume 1, 2018), 211–236 (May 2018)

    Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for Robots: Guarantees and Feedback for Robot Behavior. Annual Review of Control, Robotics, and Autonomous Systems 1(Volume 1, 2018), 211–236 (May 2018)

    work page 2018

  5. [5]

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

    Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. pp. 239–248. HSCC ’15, Association for Computing Machinery, New York, NY, USA (Apr 2015)

    work page 2015

  6. [6]

    In: 2021 IEEE International Conference on Robotics and Automation (ICRA)

    Wells, M., Kingston, Z., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: Finite-Horizon Synthesis for Probabilistic Manipulation Domains. In: 2021 IEEE International Conference on Robotics and Automation (ICRA). pp. 6336–6342 (May 2021)

    work page 2021

  7. [7]

    In: Al Faruque, M.A., Canedo, A

    Deshmukh, J.V., Sankaranarayanan, S.: Formal Techniques for Verification and Testing of Cyber-Physical Systems. In: Al Faruque, M.A., Canedo, A. (eds.) Design Automation of Cyber-Physical Systems, pp. 69–105. Springer International Publishing, Cham (2019)

    work page 2019

  8. [8]

    LeeVaraiya.org, second edn

    Lee, E.A., Varaiya, P.: Structure and Interpretation of Signals and Systems. LeeVaraiya.org, second edn. (2011)

    work page 2011

Show all 71 references
  1. [9]

    In: 18th Annual Symposium on Foundations of Computer Science (Sfcs 1977)

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (Sfcs 1977). pp. 46–57 (Oct 1977)

    1977

  2. [10]

    In: Majumdar, R., Kunčak, V

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Springer International Publishing, Cham (2017)

    2017

  3. [11]

    Ehlers, R.: Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (Aug 2017)

    2017

  4. [12]

    In: Advances in Neural Information Processing Systems

    Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient Formal Safety Analysis of Neural Networks. In: Advances in Neural Information Processing Systems. vol. 31. Curran Associates, Inc. (2018)

    2018

  5. [13]

    In: Proceedings of the 35th International Conference on Machine Learning

    Weng, L., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Daniel, L., Boning, D., Dhillon, I.: Towards Fast Computation of Certified Robustness for ReLU Networks. In: Proceedings of the 35th International Conference on Machine Learning. pp. 5276–5285. PMLR (Jul 2018)

    2018

  6. [14]

    In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC)

    Bansal, S., Chen, M., Herbert, S., Tomlin, C.J.: Hamilton-Jacobi reachability: A brief overview and recent advances. In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC). pp. 2242–2253 (Dec 2017)

    2017

  7. [15]

    IEEE Transactions on Automatic Control 50(7), 947–957 (Jul 2005)

    Mitchell, I., Bayen, A., Tomlin, C.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on Automatic Control 50(7), 947–957 (Jul 2005)

    2005

  8. [16]

    In: Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018) (2018)

    Akintunde, M.E., Lomuscio, A., Maganti, L., Pirovano, E.: Reachability Analysis for Neural Agent-Environment Systems. In: Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018) (2018)

    2018

  9. [17]

    In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

    Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: Verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. pp. 169–178. HSCC ’19, Associat...

    2019

  10. [18]

    ACM Trans

    Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verifying the Safety of Autonomous Systems with Neural Network Controllers. ACM Trans. Embed. Comput. Syst. 20(1), 7:1–7:26 (Dec 2020)

    2020

  11. [19]

    Xiang, W., Johnson, T.T.: Reachability Analysis and Safety Verification for Neural Network Control Systems (May 2018)

    2018

  12. [20]

    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s Decidable about Hybrid Automata? Journal of Computer and System Sciences 57(1), 94–124 (Aug 1998)

    1998

  13. [21]

    Journal of Artificial Intelligence Research 72, 377–428 (Oct 2021)

    Corso, A., Moss, R., Koren, M., Lee, R., Kochenderfer, M.: A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems. Journal of Artificial Intelligence Research 72, 377–428 (Oct 2021)

    2021

  14. [22]

    Theoretical Computer Science 410(42), 4262–4291 (Sep 2009) , Vol

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410(42), 4262–4291 (Sep 2009) , Vol. 1, No. 1, Article . Publication date: December 2024. 24 Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki...

    2009

  15. [23]

    In: Kroening, D., Păsăreanu, C.S

    Akazaki, T., Hasuo, I.: Time Robustness in MTL and Expressivity in Hybrid System Falsification. In: Kroening, D., Păsăreanu, C.S. (eds.) Computer Aided Verification. pp. 356–374. Springer International Publishing, Cham (2015)

    2015

  16. [24]

    Real-Time Systems 2(4), 255–299 (Nov 1990)

    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (Nov 1990)

    1990

  17. [25]

    In: Lakhnech, Y., Yovine, S

    Maler, O., Nickovic, D.: Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. pp. 152–166. Springer, Berlin, Heidelberg (2004)

    2004

  18. [26]

    Ramezani, Z.: On Optimization-Based Falsification of Cyber Physical Systems. Ph.D. thesis, Chalmers University of Technology, Göteborg (2022)

    2022

  19. [27]

    ACM Trans

    Deshmukh, J., Horvat, M., Jin, X., Majumdar, R., Prabhu, V.S.: Testing Cyber-Physical Systems through Bayesian Optimization. ACM Trans. Embed. Comput. Syst. 16(5s), 170:1–170:18 (Sep 2017)

    2017

  20. [28]

    In: 2018 IEEE International Conference on Robotics and Automation (ICRA)

    Ghosh, S., Berkenkamp, F., Ranade, G., Qadeer, S., Kapoor, A.: Verifying Controllers Against Adversarial Examples with Bayesian Optimization. In: 2018 IEEE International Conference on Robotics and Automation (ICRA). pp. 7306–7313 (May 2018)

    2018

  21. [29]

    In: IEEE International Conference on Automation Science and Engineering (CASE)

    Mathesen, L., Pedrielli, G., Fainekos, G.: Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements. In: IEEE International Conference on Automation Science and Engineering (CASE). pp. 732–737 (Aug 2021)

    2021

  22. [30]

    In: Dillig, I., Tasiran, S

    Zhang, Z., Hasuo, I., Arcaini, P.: Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 401–420. Springer International Publishing, Cham (2019)

    2019

  23. [31]

    Ramezani, Z., Šehić, K., Nardi, L., Åkesson, K.: Falsification of Cyber-Physical Systems using Bayesian Optimization (Feb 2023)

    2023

  24. [32]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(8), 2393–2406 (Aug 2022)

    Ramezani, Z., Claessen, K., Smallbone, N., Fabian, M., Åkesson, K.: Testing Cyber–Physical Systems Using a Line- Search Falsification Method. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(8), 2393–2406 (Aug 2022)

    2022

  25. [33]

    ACM Trans

    Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 12(2s), 95:1–95:30 (May 2013)

    2013

  26. [34]

    In: 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)

    Aerts, A., Tong Minh, B., Mousavi, M.R., Reniers, M.A.: Temporal Logic Falsification of Cyber-Physical Systems: An Input-Signal-Space Optimization Approach. In: 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). pp. 214–223 (...

    2018

  27. [35]

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

    Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. pp. 125–134. HSCC ’12, Association for Computing Mach...

    2012

  28. [36]

    Journal of Air Transportation 24(2), 55–62 (Apr 2016)

    Kim, Y., Kochenderfer, M.J.: Improving Aircraft Collision Risk Estimation Using the Cross-Entropy Method. Journal of Air Transportation 24(2), 55–62 (Apr 2016)

    2016

  29. [37]

    IEEE Control Systems Magazine 23(4), 49–57 (Aug 2003)

    Zhao, Q., Krogh, B., Hubbard, P.: Generating test inputs for embedded control systems. IEEE Control Systems Magazine 23(4), 49–57 (Aug 2003)

    2003

  30. [38]

    In: Proceedings of IEEE International Conference on Evolutionary Computation

    Hansen, N., Ostermeier, A.: Adapting arbitrary normal mutation distributions in evolution strategies: The covariance matrix adaptation. In: Proceedings of IEEE International Conference on Evolutionary Computation. pp. 312–317 (May 1996)

    1996

  31. [39]

    IEEE Transactions on Software Engineering 49(4), 1842–1859 (Apr 2023)

    Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage Criteria. IEEE Transactions on Software Engineering 49(4), 1842–1859 (Apr 2023)

    2023

  32. [40]

    Dreossi, T., Donzé, A., Seshia, S.A.: Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. J. Autom. Reason. 63(4), 1031–1053 (Dec 2019)

    2019

  33. [41]

    Annual Review of Control, Robotics, and Autonomous Systems 7(Volume 7, 2024), 285–310 (Jul 2024)

    Orthey, A., Chamzas, C., Kavraki, L.E.: Sampling-Based Motion Planning: A Comparative Review. Annual Review of Control, Robotics, and Autonomous Systems 7(Volume 7, 2024), 285–310 (Jul 2024)

    2024

  34. [42]

    IEEE Access 2, 56–77 (2014)

    Elbanhawi, M., Simic, M.: Sampling-Based Robot Motion Planning: A Review. IEEE Access 2, 56–77 (2014)

    2014

  35. [43]

    The International Journal of Robotics Research (Nov 2008)

    Cheng, P., Kumar, V.: Sampling-based Falsification and Verification of Controllers for Continuous Dynamic Systems. The International Journal of Robotics Research (Nov 2008)

    2008

  36. [44]

    Proceedings of the International Conference on Automated Planning and Scheduling 33, 2–6 (Jul 2023)

    Aineto, D., Scala, E., Onaindia, E., Serina, I.: Falsification of Cyber-Physical Systems Using PDDL+ Planning. Proceedings of the International Conference on Automated Planning and Scheduling 33, 2–6 (Jul 2023)

    2023

  37. [45]

    Formal Methods in System Design 34(2), 157–182 (Apr 2009)

    Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: From verification to falsification by combining motion planning and discrete search. Formal Methods in System Design 34(2), 157–182 (Apr 2009)

    2009

  38. [46]

    International Journal on Software Tools for Technology Transfer 15(4), 305–320 (Aug 2013)

    Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. International Journal on Software Tools for Technology Transfer 15(4), 305–320 (Aug 2013)

    2013

  39. [47]

    In: Erdmann, M., Overmars, M., Hsu, D., van der Stappen, F

    Esposito, J.M., Kim, J., Kumar, V.: Adaptive RRTs for Validating Hybrid Robotic Control Systems. In: Erdmann, M., Overmars, M., Hsu, D., van der Stappen, F. (eds.) Algorithmic Foundations of Robotics VI, pp. 107–121. Springer, Berlin, Heidelberg (2005) , Vol. 1, No. 1, Article...

    2005

  40. [48]

    In: 2019 IEEE Intelligent Transportation Systems Conference (ITSC)

    Tuncali, C.E., Fainekos, G.: Rapidly-exploring Random Trees for Testing Automated Vehicles. In: 2019 IEEE Intelligent Transportation Systems Conference (ITSC). pp. 661–666 (Oct 2019)

    2019

  41. [49]

    ACM Trans

    Ernst, G., Sedwards, S., Zhang, Z., Hasuo, I.: Falsification of Hybrid Systems Using Adaptive Probabilistic Search. ACM Trans. Model. Comput. Simul. 31(3), 18:1–18:22 (Jul 2021)

    2021

  42. [50]

    IEEE Transactions on Software Engineering SE-3(2), 125–143 (Mar 1977)

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

    1977

  43. [51]

    Journal of Artificial Intelligence Research 20, 61–124 (Dec 2003)

    Fox, M., Long, D.: PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains. Journal of Artificial Intelligence Research 20, 61–124 (Dec 2003)

    2003

  44. [52]

    In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence

    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. pp. 854–860. IJCAI ’13, AAAI Press, Beijing, China (Aug 2013)

    2013

  45. [53]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(11), 2894–2905 (Nov 2018)

    Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(11), 2894–2905 (Nov 2018)

    2018

  46. [54]

    In: 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC)

    Julian, K.D., Lee, R., Kochenderfer, M.J.: Validation of image-based neural network controllers through adaptive stress testing. In: 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC). pp. 1–7. IEEE (2020)

    2020

  47. [55]

    IEEE Transactions on Software Engineering 47(12), 2823–2840 (Dec 2021)

    Yamagata, Y., Liu, S., Akazaki, T., Duan, Y., Hao, J.: Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning. IEEE Transactions on Software Engineering 47(12), 2823–2840 (Dec 2021)

    2021

  48. [56]

    In: 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)

    Ernst, G., Arcaini, P., Bennani, I., Chandratre, A., Donzé, A., Fainekos, G., Frehse, G., Gaaloul, K., Inoue, J., Khandait, T., Mathesen, L., Menghi, C., Pedrielli, G., Pouzet, M., Waga, M., Yaghoubi, S., Yamagata, Y., Zhang, Z.: ARCH-COMP 2021 Category Report: Falsification w...

    2021

  49. [57]

    In: Abdulla, P.A., Leino, K.R.M

    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 254–257. Springer, Berlin, Heidelbe...

    2011

  50. [58]

    In: Touili, T., Cook, B., Jackson, P

    Donzé, A.: Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. pp. 167–170. Springer, Berlin, Heidelberg (2010)

    2010

  51. [59]

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

    Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control. pp. 253–262. HSCC ’14, Association for Computing Machinery, New York, NY, USA...

    2014

  52. [60]

    SIGBED Rev

    Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24–33 (Mar 2017)

    2017

  53. [61]

    In: Dillig, I., Tasiran, S

    Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez-Chanlatte, M., Seshia, S.A.: VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 432–442. Sp...

    2019

  54. [62]

    Machine Learning 112(10), 3805–3849 (Oct 2023)

    Fremont, D.J., Kim, E., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: A language for scenario specification and data generation. Machine Learning 112(10), 3805–3849 (Oct 2023)

    2023

  55. [63]

    The International Journal of Robotics Research 35(5), 528–564 (Apr 2016)

    Li, Y., Littlefield, Z., Bekris, K.E.: Asymptotically optimal sampling-based kinodynamic planning. The International Journal of Robotics Research 35(5), 528–564 (Apr 2016)

    2016

  56. [64]

    In: Ang, M.H., Khatib, O., Siciliano, B

    Cortés, J., Siméon, T.: Sampling-Based Tree Planners (RRT, EST, and Variations). In: Ang, M.H., Khatib, O., Siciliano, B. (eds.) Encyclopedia of Robotics, pp. 1–9. Springer, Berlin, Heidelberg (2020)

    2020

  57. [65]

    The International Journal of Robotics Research 20(5), 378–400 (May 2001)

    LaValle, S.M., Kuffner, J.J.: Randomized Kinodynamic Planning. The International Journal of Robotics Research 20(5), 378–400 (May 2001)

    2001

  58. [66]

    The International Journal of Robotics Research 21(3), 233–255 (Mar 2002)

    Hsu, D., Kindel, R., Latombe, J.C., Rock, S.: Randomized Kinodynamic Motion Planning with Moving Obstacles. The International Journal of Robotics Research 21(3), 233–255 (Mar 2002)

    2002

  59. [67]

    IEEE Transactions on Robotics 28(1), 116–131 (Feb 2012)

    Sucan, I.A., Kavraki, L.E.: A Sampling-Based Tree Planner for Systems With Complex Dynamics. IEEE Transactions on Robotics 28(1), 116–131 (Feb 2012)

    2012

  60. [68]

    In: Software Challenges in Formal Methods for Robotics (FMR) Workshop, in Conjunction with ICRA 2024

    Elimelech, K., Lahijanian, M., Vardi, M.Y., Kavraki, L.E.: LiteRacer: A lightweight autonomous vehicle simulator for benchmarking and development of formal verification techniques. In: Software Challenges in Formal Methods for Robotics (FMR) Workshop, in Conjunction with ICRA ...

    2024

  61. [69]

    Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: OpenAI Gym (Jun 2016)

    2016

  62. [70]

    Journal of Machine Learning Research 22(268), 1–8 (2021)

    Raffin, A., Hill, A., Gleave, A., Kanervisto, A., Ernestus, M., Dormann, N.: Stable-Baselines3: Reliable Reinforcement Learning Implementations. Journal of Machine Learning Research 22(268), 1–8 (2021)

    2021

  63. [71]

    re-root the tree,

    Nogueira, F.: Bayesian Optimization: Open source constrained global optimization tool for Python (2014/) , Vol. 1, No. 1, Article . Publication date: December 2024. 26 Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi A Algorithms Algorithmfalsification_...

    2014

Pith tools

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