{"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__behavioral_economics","selection_stratum":"REJECTION_LOW_BAND_AUDIT","search_queries":["behavioral economics formal verification adaptive decision models reachability model checking","human behavior model checking cognitive models formal verification probabilistic","site:prismmodelchecker.org manual reachability MDP probabilistic model checking","policy behavioural science prediction uncertainty official guidance model limitations","site:gov.uk behavioural insights policy evaluation uncertainty prediction guidance randomized controlled trials","site:oecd.org behavioural science public policy evaluation uncertainty model prediction","undecidability reachability counter machines primary paper halting problem transition systems","site:prismmodelchecker.org manual model finite states model checking limitations state space","arxiv two counter machine reachability undecidable halting reduction finite state restricted decidable model checking","site:bls.gov ooh software developers median pay 2025 computer research scientists","formal verification cognitive models human behavior primary paper model checking limitations empirical accuracy"],"sources":[{"source_id":"S1","title":"Test, Learn, Adapt: Developing Public Policy with Randomised Controlled Trials","publisher":"UK Cabinet Office and Behavioural Insights Team","url":"https://www.gov.uk/government/publications/test-learn-adapt-developing-public-policy-with-randomised-controlled-trials","source_class":"OFFICIAL_GUIDANCE","publication_date":"2012-06-14","accessed_at":"2026-08-02","claims_supported":["Official behavioral-policy guidance emphasizes specifying outcomes and comparing interventions with controls through randomized evaluation.","The opened guidance does not request an exact, terminating predictor over every adaptive behavioral model."]},{"source_id":"S2","title":"Good practice principles for ethical behavioural science in public policy","publisher":"OECD Publishing","url":"https://doi.org/10.1787/e19a9be9-en","source_class":"OFFICIAL_GUIDANCE","publication_date":"2022-10-05","accessed_at":"2026-08-02","claims_supported":["Behavioral science is used in public policy and raises ethical considerations from scoping through scaling.","Practitioners and policymakers are identifiable stakeholders responsible for ethical use.","The guidance stresses an accurate rather than imagined understanding of human behavior."]},{"source_id":"S3","title":"Probabilistic Model Checking for Complex Cognitive Tasks: A Case Study in Human-Robot Interaction","publisher":"arXiv","url":"https://arxiv.org/abs/1610.09409","source_class":"PRIMARY_RESEARCH","publication_date":"2016-10-28","accessed_at":"2026-08-02","claims_supported":["Prior research automatically converts weighted Q-table human-behavior models into MDPs for fixed scenarios and uses probabilistic model checking to predict modeled behavior.","The method represents underspecified human behavior and computes reachability probabilities with PRISM-family tools.","The prototype encountered substantial state-space and runtime costs, including a reported 16-million-state example.","The paper distinguishes results about a behavioral model from direct empirical guarantees about people."]},{"source_id":"S4","title":"Formal Verification of Cognitive Models","publisher":"AAAI Press","url":"https://cdn.aaai.org/FLAIRS/2006/Flairs06-082.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"2006","accessed_at":"2026-08-02","claims_supported":["Automated verification of cognitive models against formal competency and cognitive specifications is established prior art.","The approach constructs a graph over model traces and checks patterns and conflicts automatically.","The paper notes difficulty fully specifying ill-structured cognitive tasks and the need to interpret over-approximating verification results carefully."]},{"source_id":"S5","title":"PRISM Manual: Computation Engines","publisher":"PRISM Model Checker, University of Oxford","url":"https://www.prismmodelchecker.org/manual/ConfiguringPRISM/ComputationEngines","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"2021-03-18","accessed_at":"2026-08-02","claims_supported":["PRISM offers approximate statistical model checking based on simulation as well as limited exact numerical model checking.","Some PRISM analyses explicitly reduce models to finite-state MDPs.","Exact arithmetic support is restricted to relatively small models, and engine choice can impose language and property restrictions."]},{"source_id":"S6","title":"Bounded Reachability Problems are Decidable in FIFO Machines","publisher":"Logical Methods in Computer Science","url":"https://arxiv.org/abs/2105.06723","source_class":"PRIMARY_RESEARCH","publication_date":"2022-01-20","accessed_at":"2026-08-02","claims_supported":["General systems with unbounded FIFO channels can simulate Turing machines, making many verification properties undecidable.","An input-bounded restriction yields decidability for reachability, termination, deadlock, and related properties.","The authors explicitly present bounded restrictions as a foundation for verification tools."]},{"source_id":"S7","title":"Certified Decision Procedures for Two-Counter Machines","publisher":"Schloss Dagstuhl – Leibniz-Zentrum für Informatik","url":"https://doi.org/10.4230/LIPIcs.FSCD.2022.16","source_class":"PRIMARY_RESEARCH","publication_date":"2022-08-01","accessed_at":"2026-08-02","claims_supported":["Two-counter machines provide a simple universal computation model, and halting is undecidable for the declared CM2 instruction set.","Small changes in machine semantics or instruction sets can change decidability results.","The work demonstrates machine-checked termination and correctness proofs for restricted decision procedures using Coq."]},{"source_id":"S8","title":"Computer and Information Research Scientists: Occupational Outlook Handbook","publisher":"U.S. Bureau of Labor Statistics","url":"https://www.bls.gov/ooh/computer-and-information-technology/computer-and-information-research-scientists.htm","source_class":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2025-08-28","accessed_at":"2026-08-02","claims_supported":["The May 2024 median annual wage for computer and information research scientists was $140,910, with substantial variation by industry.","These specialists develop theories, models, languages, tools, and software experiments and commonly collaborate across disciplines.","The wage data provide a public labor-cost anchor but not a direct project quote."]}],"problem_evidence":{"support":"NOT_FOUND","rationale":"The bounded search found official behavioral-policy practice centered on empirical testing, predefined outcomes, controls, context, and ethical governance, but no specification demanding a correct, terminating verdict for every finitely described adaptive behavioral model. This does not prove such requests never occur; it means the candidate's asserted domain problem remains externally unsupported in the searched record. S1 and S2 instead describe experimental and evidence-informed practice.","source_ids":["S1","S2"]},"stakeholder_evidence":{"support":"WEAK","rationale":"OECD guidance establishes policymakers and behavioral-science practitioners as real stakeholders with responsibility from scoping through scaling, and S1 identifies policy evaluators as users of behavioral evidence. No source identifies an organization willing to adopt or authorize the proposed computability-boundary router, however.","source_ids":["S1","S2"]},"prior_art":{"proximity":"ADJACENT_PRIOR_ART","closest_analogues":[{"name":"Probabilistic model checking of weighted Q-table human-behavior models","similarity":"S3 already formalizes human behavioral models as MDPs, includes behavioral underspecification, evaluates reachability probabilities, and uses automated model checking to support decisions in adaptive human-machine settings.","remaining_difference":"It operates on a declared model family and fixed scenarios; it does not present a policy-facing preflight that proves an unrestricted behavioral language undecidable, enforces fragment membership, or requires explicit UNKNOWN propagation for out-of-scope inputs.","source_ids":["S3"]},{"name":"Automated formal verification of cognitive models","similarity":"S4 already specifies cognitive-model requirements and automatically verifies model traces against competency and cognitive constraints.","remaining_difference":"It is model-correctness verification rather than a computability-boundary analysis of universal eventual-outcome prediction, and it does not implement exact/bounded/UNKNOWN routing.","source_ids":["S4"]},{"name":"PRISM exact, approximate, and finite-state analysis modes","similarity":"S5 supplies existing exact and simulation-based modes, finite-state reductions, modeling-language restrictions, and quantitative reachability analysis—the main technical ingredients of the proposed fallback modes.","remaining_difference":"The documentation does not supply a behavioral-policy governance layer that checks language membership before analysis or prevents timeout and unsupported results from becoming binary policy claims.","source_ids":["S5"]},{"name":"Bounded restrictions recovering decidability in infinite-state verification","similarity":"S6 closely matches the structural mechanism: an unrestricted computational model has undecidable properties, while an enforceable bounded class recovers decidable reachability and termination analyses.","remaining_difference":"The result concerns FIFO machines, not behavioral-economic models, and therefore does not establish the required embedding or preservation proof for any behavioral language.","source_ids":["S6","S7"]}],"distinctive_claim_remaining":"Relative to S3-S7, the remaining testable claim is a behavioral-policy-specific workflow for one explicitly defined adaptive language that independently verifies a halting-preserving reduction, mechanically enforces membership in useful decidable fragments, routes all other cases to bounded or UNKNOWN outputs, and audits that downstream reports preserve those labels. None of those sources establishes the combined claim for behavioral policy.","confidence":"HIGH"},"implementation_evidence":{"support":"MODERATE","rationale":"The ingredients are implementable separately: human-behavior models have been translated into MDPs and checked with prototypes; PRISM supports finite-state, simulation, and limited exact modes; bounded verification classes and proof-assistant-certified decision procedures exist. Evidence is still missing for the candidate's particular behavioral language, reduction, fragment checker, useful coverage, and integrated output-governance workflow. S3 also demonstrates that state-space growth can make even decidable analyses costly.","source_ids":["S3","S5","S6","S7"]},"scores":{"meaningful_impact":{"score":2,"rationale":"Preventing definitive claims unsupported by behavioral evidence or model semantics could improve responsible policy analysis, consistent with S1-S2. No source establishes incidence, affected population, expenditure, or realized harm from universal exact-predictor demands, so impact remains speculative.","source_ids":["S1","S2"]},"stakeholder_pull":{"score":1,"rationale":"Real behavioral-policy practitioners and policymakers exist, but the search found no request, procurement, adopter commitment, or specification for this computability-boundary service. Official practice found in S1 emphasizes comparative empirical evaluation instead.","source_ids":["S1","S2"]},"incremental_advantage":{"score":3,"rationale":"A checked scope router and mandatory UNKNOWN output would add a useful governance layer beyond existing behavioral model checking and simulation, especially where a language crosses a decidability boundary. Its coverage and decision value have not been demonstrated.","source_ids":["S3","S5","S6","S7"]},"distinctiveness_plausibility":{"score":2,"rationale":"Formal verification of cognitive and human-behavior models, multiple analysis modes, and bounded restrictions recovering decidability are all prior art. Only the behavioral-policy-specific combination and enforced abstention pathway remain potentially distinctive.","source_ids":["S3","S4","S5","S6"]},"technical_implementability":{"score":3,"rationale":"A narrow synthetic prototype is feasible using existing model-checking and proof-assistant methods, but semantics are decisive and cannot be assumed: S7 shows instruction-set changes can alter decidability. State-space growth and limited exact-mode scalability are additional constraints.","source_ids":["S3","S5","S7"]},"adoption_authority_feasibility":{"score":2,"rationale":"S2 establishes policymakers and practitioners as responsible stakeholders, but no real organization or joint behavioral-methods/formal-verification owner has accepted authority for the proposed workflow. Intervention authority must remain separate from model-analysis approval.","source_ids":["S2"]},"evidence_readiness":{"score":2,"rationale":"Relevant formal methods, tools, and behavioral-model precedents are documented, but the two decisive items—evidence of a real universal requirement and a checked reduction for a declared behavioral language—remain absent.","source_ids":["S1","S3","S4","S6","S7"]},"safety_net_benefit":{"score":4,"rationale":"Explicit UNKNOWN handling, bounded claims, and separation of model verification from empirical intervention evaluation align with the ethical and experimental cautions in S1-S2 and with the limitations visible in S3-S5. The benefit remains conditional on downstream systems preserving labels.","source_ids":["S1","S2","S3","S5"]},"scalability":{"score":2,"rationale":"The routing concept is reusable, but reductions and fragment checkers are language-specific. S3 reports large state spaces and long runtimes, while S5 limits exact support to relatively small models, indicating weak evidence for economical scaling.","source_ids":["S3","S5","S7"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"50K_TO_250K","scope":"A six-to-twelve-week evidence program covering a small specification/interview corpus; behavioral-model and formal-methods labor; definition of one language; one reduction attempt and independent proof review; a finite-state membership checker; synthetic test data; computing, proof-assistant and model-checker tooling; ethics and governance review; coordination; reproducibility documentation; and comparative evaluation against bounded simulation.","confidence":"MODERATE","assumptions":["Two to four specialists contribute part-time rather than forming a full production team.","No sensitive individual data, live intervention, or regulated eligibility decision is involved.","Open-source proof and model-checking software is adequate.","The BLS research-scientist wage is only a labor anchor; calendar-2026 benefits, overhead, specialist premiums, coordination, and evaluation are included through the broad band.","The corpus is capped and independent proof review is limited to one declared language."],"source_ids":["S3","S5","S7","S8"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Convert a validated prototype into one governed organizational service: production parser and semantics; enforceable fragment checker; exact, bounded, and UNKNOWN routing; audit logs; security and privacy review; software and compute environments; documentation; integration with one modeling workflow; user-interface labeling; compliance coordination; and pre-launch validation.","confidence":"LOW","assumptions":["At least one real universal requirement and one useful restricted fragment survive first evidence.","One organization and one principal model language are in scope.","No automated policy or individual-level decision authority is granted.","Costs include engineering, behavioral-methods review, formal assurance, security, compliance, project management, software, equipment, and contingency for state-space performance work.","No proprietary behavioral dataset acquisition is required."],"source_ids":["S2","S3","S5","S8"]},"operational_launch":{"band_2026_usd":"250K_TO_1M","scope":"Independent assurance, adversarial and failure-label testing, evaluation on a broader disclosed corpus, downstream UNKNOWN-propagation tests, governance approvals, incident and rollback procedures, staff training, coordination with one adopter, compute provisioning, documentation, and a monitored non-intervention launch.","confidence":"LOW","assumptions":["A willing adopter and accountable review owners are available.","Launch remains model-analytic and excludes live behavioral interventions and individual decisions.","The evaluation corpus can be licensed or created without sensitive-data compliance burdens.","Restricted-mode coverage and performance are sufficient to justify launch.","State-space costs resemble research prototypes rather than requiring specialized high-performance infrastructure."],"source_ids":["S2","S3","S5","S8"]},"annual_recurring":{"band_2026_usd":"50K_TO_250K","scope":"Part-time formal-methods and behavioral-model maintenance; model-language change review; regression and assurance testing; monitoring of UNKNOWN and timeout labels; security, compliance, software and compute maintenance; user support; audit and governance meetings; and annual evaluation for one deployment.","confidence":"LOW","assumptions":["One organization and a small number of stable dialects remain in scope.","Major new reductions, proof programs, integrations, proprietary data purchases, and live intervention evaluation are excluded.","Open-source core tooling remains usable.","Human review is retained for scope changes and policy-facing claims.","The broad band includes labor overhead and recurring coordination, software, equipment, compliance, and evaluation."],"source_ids":["S2","S5","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"NO","reason":"The bounded search found no external evidence of an actual behavioral-policy requirement for an exact, terminating, class-wide outcome predictor. Official sources instead describe empirical comparison, contextual evidence, and ethical scoping. Absence in this search is not proof of global absence.","source_ids":["S1","S2"]},"externally_credible_adopter_or_authorizer":{"status":"UNCERTAIN","reason":"Policymakers and behavioral-science practitioners are credible affected stakeholders, but no source names a willing adopter or an organization that assigns formal-verification authority for behavioral-model analysis.","source_ids":["S1","S2"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The incremental claim can be falsified for one declared language by checking the reduction, fragment-membership algorithm, termination and labels, and comparative coverage. Existing work supplies close comparison methods without establishing this combined behavioral-policy claim.","source_ids":["S3","S4","S5","S6","S7"]},"bounded_next_evidence_step":{"status":"YES","reason":"A capped document/interview screen followed conditionally by one synthetic language, one reduction attempt, one restricted checker, and a disclosed comparison corpus is bounded, reproducible, and does not require intervention on people.","source_ids":["S1","S2","S3","S6","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The proposed evidence work can remain synthetic and model-analytic, exclude individual or intervention decisions, preserve UNKNOWN, and use ethics review and explicit rollback. No source identifies a safety necessity for live deployment.","source_ids":["S1","S2"]},"credible_cost_scope_and_range":{"status":"YES","reason":"The bands include labor, data or synthetic-corpus work, software, compute and equipment, security and compliance, coordination, independent assurance, training, and evaluation. BLS supplies a labor anchor, while prior prototypes and official tooling document material compute and implementation scope; deployment bands remain low confidence because no adopter specification or quote exists.","source_ids":["S3","S5","S8"]}},"next_evidence_step":"Run a capped two-stage, non-deployment study. Stage 1: within six weeks, review 20 purposively sampled behavioral-policy specifications or analytic procurements and interview no more than eight policy/modeling owners; compare the prevalence of exact, terminating, class-wide outcome demands with finite-horizon probabilistic or empirical-evaluation requirements. The problem is falsified for advancement if no sampled requirement demands total exact prediction or if every apparent case becomes bounded when clarified. Only if at least one genuine case survives, Stage 2 may formalize that case's single model language in a synthetic sandbox, independently check one halting-preserving reduction, implement one finite-state membership checker, and compare exact, bounded, simulation, and UNKNOWN outputs on at most 50 disclosed models. Falsify the intervention if the reduction fails, membership is not enforceable, a promised mode fails to terminate or preserve its label, or restricted modes add no useful correct coverage over bounded simulation.","blocking_evidence":["No actual specification or stakeholder request demanding exact, terminating, class-wide behavioral-outcome prediction was found in S1-S2 or the bounded search.","No declared behavioral-language semantics or computable source-to-target mapping has been supplied; general undecidability results in S6-S7 do not transfer automatically.","No independently checked proof establishes that target behavior or welfare attainment preserves halting for the candidate language.","No implemented fragment checker demonstrates enforceable membership, termination, coverage, and performance against the behavioral-model precedents in S3-S5.","No evidence shows a real adopter will preserve UNKNOWN and model-level qualification in downstream policy reports.","No empirical evidence establishes that formal model correctness improves predictions of people or welfare outcomes; S1-S2 instead support separate empirical evaluation."],"research_disposition":"PROBLEM_PREVALENCE_STUDY","world_novelty_boundary":"No world-novelty conclusion is made or warranted. This bounded search of S1-S8 found established adjacent prior art in cognitive-model verification, probabilistic human-behavior model checking, exact and statistical analysis modes, and restrictions that recover decidability. It did not establish that the remaining behavioral-policy-specific combination is novel anywhere in the world, nor would failure to find a closer match prove world novelty."}