{"schema_version":1,"research_id":"eoa_inverse_innovation_exp03_external48_20260801","source_assessment_id":"eoa_inverse_innovation_exp03_opportunity320_20260801","cell_id":"computability_boundary_mapping__systems_cybernetics","selection_stratum":"DEPLOYABLE_PRIORITY","search_queries":["hybrid automata reachability undecidable decidable classes Henzinger primary paper PDF","undecidable problems control systems reachability feedback system Turing machine primary paper","SpaceEx scalable verification hybrid systems CAV 2011 paper PDF","ARCH-COMP hybrid systems benchmark unknown result reachability 2024","KeYmaera X unknown result verification hybrid systems official documentation","NASA software assurance independent assessment safety standard official","NASA-STD-7009B Models Simulations official standard validation uncertainty"],"sources":[{"source_id":"S1","title":"What's Decidable About Hybrid Automata?","publisher":"Cornell University","url":"https://hdl.handle.net/1813/7198","source_class":"PRIMARY_RESEARCH","publication_date":"1995-09","accessed_at":"2026-08-02","claims_supported":["Hybrid-automaton reachability has a model-relative boundary: initialized rectangular automata have a terminating reachability procedure, while slight generalizations are undecidable.","The system language and restrictions are load-bearing parts of any decidability claim."]},{"source_id":"S2","title":"Complexity of Stability and Controllability of Elementary Hybrid Systems","publisher":"Automatica / Elsevier","url":"https://web.mit.edu/jnt/www/Papers/J071-99-vb-hybr.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"1999-03","accessed_at":"2026-08-02","claims_supported":["Basic stability, controllability, and reachability questions can be undecidable or computationally intractable even for simple hybrid and nonlinear system classes.","Undecidability and resource intractability are distinct diagnoses requiring different responses."]},{"source_id":"S3","title":"SpaceEx: Scalable Verification of Hybrid Systems","publisher":"Computer Aided Verification / Springer","url":"https://www-verimag.imag.fr/~tdang/Papers/CAV2011.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"2011-07","accessed_at":"2026-08-02","claims_supported":["SpaceEx implements reachability analysis for a specified class of piecewise-affine nondeterministic hybrid systems.","The method computes conservative over-approximations because exact verification is unavailable in general.","Restricted-model, guarantee-qualified reachability analysis is established prior art."]},{"source_id":"S4","title":"KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems","publisher":"KeYmaera X Project","url":"https://keymaerax.org/","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"2024-10-22","accessed_at":"2026-08-02","claims_supported":["KeYmaera X verifies specified hybrid-system properties with a small soundness-critical proof kernel.","It supports interactive, tactic-driven, and automated proof search, including partial proof interaction rather than promising a universal automatic Boolean decider."]},{"source_id":"S5","title":"ARCH-COMP23 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics","publisher":"EPiC Series in Computing / EasyChair","url":"https://easychair.org/publications/paper/T7LG","source_class":"PRIMARY_RESEARCH","publication_date":"2023-10-18","accessed_at":"2026-08-02","claims_supported":["A fixed benchmark suite and independent repeatability evaluation are established ways to compare hybrid-system verification tools.","Tool support and verification outcomes vary by benchmark, dynamics, input format, configuration, and property; reported tables include unsupported and unsuccessful cases.","A non-actuating corpus comparison with reproducible artifacts is technically credible."]},{"source_id":"S6","title":"NASA-STD-7009B: Standard for Models and Simulations","publisher":"NASA Office of the Chief Engineer","url":"https://standards.nasa.gov/standard/nasa/nasa-std-7009","source_class":"STANDARD","publication_date":"2024-03-05","accessed_at":"2026-08-02","claims_supported":["Model and simulation acceptance criteria must be defined by the program or project and approved by delegated technical authority.","Model credibility, validation, verification, uncertainty qualification, and intended use are governance obligations relevant to transferring model verdicts to real systems."]},{"source_id":"S7","title":"NASA-STD-8739.8B: Software Assurance and Software Safety Standard","publisher":"NASA Office of Safety and Mission Assurance","url":"https://swehb.nasa.gov/spaces/SITE/pages/119242809/NASA-STD-8739.8B","source_class":"STANDARD","publication_date":"2022-09-08","accessed_at":"2026-08-02","claims_supported":["Safety-critical software assurance uses rigorous analysis and testing to produce objective evidence and independent assessments.","Project management and Safety and Mission Assurance roles are responsible for resources, oversight, records, hazard-related classification, and issue closure.","Independent verification and validation requires technical, managerial, and financial independence."]}],"problem_evidence":{"support":"WEAK","rationale":"The technical failure mode is strongly supported: computability and complexity change with the declared model class, and exact general verification can fail even for comparatively simple hybrid systems. Conservative approximation and proof-based restricted analysis are consequently established. However, the bounded search found no documented assurance program exhibiting the candidate's exact empirical signature—an unrestricted, exact, terminating SAFE/UNSAFE interface that coerces timeouts or unsupported models and omits UNKNOWN or OUT_OF_SCOPE. The diagnosed target-program problem therefore remains unverified.","source_ids":["S1","S2","S3","S4","S5"]},"stakeholder_evidence":{"support":"WEAK","rationale":"Official standards establish credible project-owner, technical-authority, safety-assurance, and independent-review roles and require resources and objective evidence. They do not demonstrate adopter demand, dissatisfaction, purchasing intent, incidents caused by this exact interface, or commitment to the proposed routing workflow.","source_ids":["S6","S7"]},"prior_art":{"proximity":"ESTABLISHED_PRACTICE","closest_analogues":[{"name":"Model-relative decidability analysis for hybrid-automaton reachability","similarity":"It explicitly defines model classes, proves termination for a restricted fragment, and proves undecidability after small expressiveness changes. This is substantially the candidate's central computability-boundary mechanism.","remaining_difference":"The candidate additionally proposes an organizational interface that mechanically checks fragment admission, maintains a change-sensitive boundary record, and controls downstream interpretation of UNKNOWN and OUT_OF_SCOPE.","source_ids":["S1","S2"]},{"name":"SpaceEx conservative reachability verification","similarity":"It analyzes a declared hybrid-system class through conservative reachable-set over-approximation instead of claiming a universal exact predictor.","remaining_difference":"SpaceEx is a verification platform, whereas the residual candidate claim concerns cross-method admission, guarantee-labelled routing, timeout handling, and governance records.","source_ids":["S3"]},{"name":"KeYmaera X proof-kernel workflow","similarity":"It binds verdict confidence to formal semantics and checkable proofs while permitting interactive or incomplete proof search rather than equating failed automation with falsity.","remaining_difference":"The candidate's testable difference is automatic routing among exact, one-sided, unknown, and out-of-scope modes across an assurance program, including downstream non-coercion controls.","source_ids":["S4"]},{"name":"ARCH-COMP benchmark and repeatability workflow","similarity":"It uses fixed models, declared tool settings, result tables, unsupported cases, and independent repeatability evaluation, closely matching the proposed sandbox evidence pattern.","remaining_difference":"The candidate would specifically compare guarantee-mislabelling against a simulation-plus-timeout Boolean baseline and audit the downstream preservation of abstention states.","source_ids":["S5"]},{"name":"NASA model-credibility and independent-assurance governance","similarity":"It requires intended-use criteria, technical-authority approval, documented evidence, maintained records, resources, and independent assessment.","remaining_difference":"The standards do not prescribe the candidate's computability-boundary record, mechanical decidable-fragment checker, or four-state routing interface.","source_ids":["S6","S7"]}],"distinctive_claim_remaining":"The remaining claim is not a new computability theorem or verification method. It is that, in an assurance program first shown to coerce simulation timeouts or unsupported cases into Boolean viability verdicts, mechanically enforced fragment admission plus guarantee-labelled SAFE, UNSAFE, UNKNOWN, and OUT_OF_SCOPE routing, a maintained boundary record, and downstream non-coercion controls will reduce guarantee mislabelling while preserving exact correctness on admitted cases. This integrated organizational effect was not established by the bounded search.","confidence":"HIGH"},"implementation_evidence":{"support":"STRONG","rationale":"Published tools and benchmark campaigns demonstrate implementable model languages, proof kernels, conservative reachability algorithms, bounded corpora, declared configurations, and independently repeatable evaluation. Official standards also provide credible governance structures. These sources do not validate any particular concrete-to-abstract system mapping or the proposed workflow's effect on organizational decisions.","source_ids":["S3","S4","S5","S6","S7"]},"scores":{"meaningful_impact":{"score":4,"rationale":"Preventing an unsound safety verdict can materially reduce hazard exposure in controlled systems, but no target-program occurrence rate or incident evidence was found.","source_ids":["S2","S6","S7"]},"stakeholder_pull":{"score":2,"rationale":"Assurance and technical-authority roles have externally documented reasons to value trustworthy evidence, but direct demand for this exact workflow was not found.","source_ids":["S6","S7"]},"incremental_advantage":{"score":3,"rationale":"The workflow directly improves semantic honesty relative to timeout-based Boolean judgment, but restricted verification, conservative approximation, partial proofs, and unsupported-case reporting already exist; the incremental claim is mainly integration and enforcement.","source_ids":["S1","S3","S4","S5"]},"distinctiveness_plausibility":{"score":2,"rationale":"Most technical and governance components are established practice. Only their proposed coupling into a maintained, mechanically enforced, downstream non-coercion workflow remains plausibly distinctive.","source_ids":["S1","S3","S4","S5","S6","S7"]},"technical_implementability":{"score":4,"rationale":"Existing tools and reproducible benchmark practice make a one-language, one-predicate, non-actuating pilot feasible. Fragment proof, admission correctness, and abstraction soundness remain case-specific obligations.","source_ids":["S3","S4","S5"]},"adoption_authority_feasibility":{"score":4,"rationale":"Official standards assign relevant authority, oversight, evidence, and independent-assessment responsibilities, making bounded authorization structurally credible even though no specific adopter has committed.","source_ids":["S6","S7"]},"evidence_readiness":{"score":3,"rationale":"A fixed corpus, exhaustive reference for a finite fragment, repeatability artifacts, and explicit falsifiers are readily specifiable, but the target interface, corpus, formal contract, and independent reviewers have not been secured.","source_ids":["S5","S7"]},"safety_net_benefit":{"score":4,"rationale":"Explicit abstention, conservative analysis, retained controls, technical-authority review, and independent assessment can reduce false-certification risk. Abstraction mismatch and downstream coercion remain material residual risks.","source_ids":["S3","S4","S6","S7"]},"scalability":{"score":3,"rationale":"The routing and record pattern is reusable, but each language, predicate, abstraction, and expressiveness change can require specialized proof, validation, configuration, and reclassification.","source_ids":["S1","S3","S5","S6"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"50K_TO_250K","scope":"Audit one interface; acquire and sanitize its requirements, logs, and model artifacts; formalize one language and viability predicate; implement a finite-fragment checker and four-state router; build a fixed sandbox corpus and exhaustive comparator; run reproducible evaluation; document compliance and access controls; and obtain independent proof review. Includes formal-methods and assurance labor, data handling, coordination, ordinary computing equipment, software/tooling, and evaluation.","confidence":"LOW","assumptions":["Approximately two to four specialist person-months plus independent review are required.","Existing workstations or cloud compute and open or already licensed verification tools are sufficient.","No live integration, regulated submission, new specialized equipment, or proprietary data purchase is required.","No direct cost study for this exact workflow was found."],"source_ids":["S4","S5","S7"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Harden the validated workflow for one system family, including parser and fragment checker, solver integration, model and evidence repositories, access controls, audit logs, regression corpus, abstraction evidence, security and compliance review, technical-authority coordination, documentation, training, and independent validation. Includes labor, data governance, software, compute equipment, evaluation, and process integration.","confidence":"LOW","assumptions":["One organization and one approved model family are in scope.","Existing safety controls and core compute infrastructure remain in place.","The pilot passes and proof obligations for the admitted fragment close.","External certification and live-actuation integration are excluded."],"source_ids":["S3","S6","S7"]},"operational_launch":{"band_2026_usd":"250K_TO_1M","scope":"Complete production-readiness validation for one governed assurance program; secure technical-authority and independent-review acceptance; train reviewers and operators; implement UNKNOWN and OUT_OF_SCOPE escalation and non-coercion controls; monitor initial cases; and establish incident, rollback, and guarantee-withdrawal procedures. Includes labor, controlled data migration, compliance, coordination, compute/software operations, equipment support, and launch evaluation.","confidence":"LOW","assumptions":["Launch remains limited to an approved fragment and makes no universal-predictor claim.","The analyzer does not connect to actuation or replace existing safety controls.","No specialized hardware procurement or major commercial licensing is required.","A multi-site or multi-domain rollout is excluded."],"source_ids":["S5","S6","S7"]},"annual_recurring":{"band_2026_usd":"250K_TO_1M","scope":"Maintain semantics, fragment rules, tools, compute, controlled datasets, and regression artifacts; re-review proofs and model credibility after changes; audit downstream abstention handling; renew training and compliance records; coordinate incidents; preserve independent assessment; and update or withdraw stale guarantees. Includes specialist labor, software and equipment support, data governance, evaluation, and oversight.","confidence":"LOW","assumptions":["One safety program and a limited set of admitted fragments are maintained.","One to several specialist FTE-equivalents plus periodic independent review are required.","Major solver development, new system classes, and external certification are additional startup work.","No direct recurring-cost benchmark for this workflow was found."],"source_ids":["S5","S6","S7"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"UNCERTAIN","reason":"The computability-boundary failure mode is well established, but this search did not verify that a real target program makes or operationally infers the diagnosed unrestricted Boolean claim or coerces timeouts and unsupported cases.","source_ids":["S1","S2","S3","S5"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"Project management, delegated technical authority, Safety and Mission Assurance, and independent verification roles are documented official governance structures capable of authorizing a bounded study. No specific organization has committed to adoption.","source_ids":["S6","S7"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The residual claim is separable from established verification theory: enforced admission and four-state routing should reduce guarantee mislabelling relative to simulation-plus-timeout Boolean output while matching exhaustive results on every admitted case.","source_ids":["S3","S4","S5"]},"bounded_next_evidence_step":{"status":"YES","reason":"One audited interface, model language, viability predicate, finite fragment, fixed corpus, exhaustive comparator, and predeclared rejection rules form a finite, non-actuating experiment.","source_ids":["S5","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The proposed experiment retains existing controls, uses sandbox artifacts, requires delegated authority and independent review, and halts on disagreement, ambiguous admission, or unwitnessed timeout verdicts.","source_ids":["S6","S7"]},"credible_cost_scope_and_range":{"status":"YES","reason":"The scopes are bounded to one interface, language, fragment, corpus, system family, and assurance program and explicitly include labor, data, compliance, coordination, equipment, software, and evaluation. Ranges remain low-confidence because no direct cost study was found.","source_ids":["S3","S5","S6","S7"]}},"next_evidence_step":"Pre-register a non-actuating study of one real assurance interface and a fixed corpus of 100 to 300 finite-state or explicitly bounded-horizon adaptive feedback models. First test the problem falsifier by auditing whether the interface actually claims or operationally implies an exact class-wide Boolean verdict, converts timeout or unsupported input into SAFE or UNSAFE, or omits usable scope states. If that diagnosis holds, compare the existing simulation-plus-timeout route with mechanical fragment admission and SAFE, UNSAFE, UNKNOWN, and OUT_OF_SCOPE routing against exhaustive state enumeration. Reject the intervention if it fails to reduce guarantee mislabelling, disagrees with enumeration on any admitted case, yields any ambiguous membership result, or emits SAFE or UNSAFE after timeout without a checkable witness. Do not connect the study to actuation or change existing safety controls.","blocking_evidence":["A documented target requirement or interface exhibiting the diagnosed universal Boolean claim or timeout or unsupported-input coercion; without this, the problem gate remains uncertain.","A precise contract for the model language, encoding, quantifiers, computation model, permitted external information, viability envelope, and guarantee semantics.","A mechanically checkable fragment-membership procedure and independently reviewed totality and correctness proof for the selected exact fragment.","A justified concrete-to-abstract relation before transferring any sandbox verdict to a physical or operational system.","Comparative results showing fewer guarantee mislabels and zero admitted-case disagreement against exhaustive enumeration.","Evidence that downstream authorization logic preserves UNKNOWN and OUT_OF_SCOPE rather than treating them as SAFE.","Before any unrestricted impossibility claim, an independently checked answer-preserving reduction under exactly the declared contracts."],"research_disposition":"PROBLEM_PREVALENCE_STUDY","world_novelty_boundary":"This bounded search found longstanding prior art for model-relative decidability, restricted verification classes, conservative reachable-set analysis, checkable proof kernels, incomplete or unsupported-case handling, repeatable benchmark evaluation, model-credibility governance, and independent assurance. It did not establish prior use of the exact combined maintained-boundary-record, mechanical admission, four-state routing, and downstream non-coercion workflow. That residual is a testable implementation and governance difference, not a world-novelty claim."}