{"id":"W4409967420","doi":"10.1007/978-3-031-90660-2_2","title":"Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification","year":2025,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Sherbrooke","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Computer science; State diagram; State (computer science); Data structure; Theoretical computer science; Programming language; Algorithm","routes":{"ca_aff":true,"ca_fund":true,"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","open_science"],"consensus_categories":[],"category_scores_codex":[0.001668408,0.000667185,0.0006575959,0.001130926,0.0003857434,0.0008923907,0.01042833,0.0004572773,0.000008213016],"category_scores_gemma":[0.0009658866,0.0006412183,0.0001212178,0.001199539,0.0006316502,0.001558632,0.002801127,0.0009002401,0.00001726163],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.000355568,"about_ca_system_score_gemma":0.001025907,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002178147,"about_ca_topic_score_gemma":0.00008545254,"domain_scores_codex":[0.9947219,0.00008525673,0.0008656713,0.002624763,0.0009120161,0.0007903782],"domain_scores_gemma":[0.9923158,0.0009764164,0.0005871594,0.005520133,0.0004314547,0.0001690275],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000013054,0.00002081359,0.00002027983,0.0001300003,0.00001873321,0.000004642351,0.0005280051,0.005899585,0.0003868465,0.06867713,0.0001103218,0.9241906],"study_design_scores_gemma":[0.0002526456,0.0001076536,0.0002318883,0.000322233,0.0000191961,0.00001689047,1.801847e-7,0.756495,0.002528298,0.2255821,0.01377033,0.0006736122],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00005886647,0.0004274063,0.9930356,0.0006870532,0.003165156,0.00124595,0.000193976,0.0002659349,0.0009200613],"genre_scores_gemma":[0.01479902,0.0001097567,0.9826804,0.001243133,0.0004093508,0.00004390925,0.0001881281,0.00004162218,0.0004846222],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.923517,"threshold_uncertainty_score":0.9996039,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04171524278728744,"score_gpt":0.3111681039484762,"score_spread":0.2694528611611888,"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."}}