{"id":"W1976967219","doi":"10.1016/j.entcs.2005.01.045","title":"A New Approach to Upward-Closed Set Backward Reachability Analysis","year":2005,"lang":"en","type":"article","venue":"Electronic Notes in Theoretical Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":15,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Reachability; Parameterized complexity; Petri net; Binary decision diagram; Fixed point; Model checking; Intersection (aeronautics); Computer science; Set (abstract data type); Computation; Algorithm; Theoretical computer science; Stochastic Petri net; Class (philosophy); State (computer science); Mathematics; Programming language","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.00658948,0.0002912075,0.0004370997,0.0008144436,0.0002260058,0.0004100833,0.004555212,0.0001056195,0.00005122542],"category_scores_gemma":[0.0007224153,0.0002643069,0.0001665435,0.008545229,0.0008276555,0.0009861763,0.001110161,0.0005341867,0.0001538157],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00079264,"about_ca_system_score_gemma":0.0005946991,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003560726,"about_ca_topic_score_gemma":0.00001590193,"domain_scores_codex":[0.9949846,0.0004260081,0.0005715623,0.001625994,0.001004593,0.001387217],"domain_scores_gemma":[0.9967567,0.0004359183,0.0001016707,0.002075192,0.0001554277,0.0004750639],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001383462,0.00008537233,0.0001839585,0.000003301045,0.00001402409,5.328089e-7,0.0008586301,0.009446345,0.0001717434,0.7917981,0.00001737623,0.1974067],"study_design_scores_gemma":[0.000218704,0.0001770752,0.003264355,0.000006893232,0.00001979609,0.00001190609,0.000003363783,0.8913854,0.006050419,0.0980517,0.0004768967,0.0003335424],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01695202,0.00003641502,0.9782082,0.001630697,0.0001699962,0.0003875498,9.864623e-7,0.0002045855,0.002409498],"genre_scores_gemma":[0.494735,0.000002020309,0.5047705,0.0003822867,0.00008217825,0.00001326023,9.965155e-7,0.00000552171,0.000008282925],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.881939,"threshold_uncertainty_score":0.9999809,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01737028778483418,"score_gpt":0.3021167304164428,"score_spread":0.2847464426316086,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}