{"id":"W3174155805","doi":"10.1145/3464794","title":"The Reachability Problem for Two-Dimensional Vector Addition Systems with States","year":2021,"lang":"en","type":"article","venue":"Journal of the ACM","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Montréal; Université de Sherbrooke","funders":"Fonds de recherche du Québec – Nature et technologies; Engineering and Physical Sciences Research Council; Natural Sciences and Engineering Research Council of Canada; Technische Universität München; Centre National de la Recherche Scientifique; Agence Nationale de la Recherche","keywords":"Reachability; Unary operation; Bounded function; Mathematics; Reachability problem; Sequence (biology); Discrete mathematics; Path (computing); Combinatorics; Binary number; Computer science; Arithmetic","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":[],"consensus_categories":[],"category_scores_codex":[0.001872501,0.0000600523,0.0001025467,0.00001556614,0.0002345171,0.0001418154,0.001364937,0.00001985822,0.000001621428],"category_scores_gemma":[0.001316842,0.00002711166,0.00007517273,0.0001705346,0.00005004032,0.0003131191,0.0002477887,0.000146617,0.000001224008],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008336805,"about_ca_system_score_gemma":0.0001840009,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004843662,"about_ca_topic_score_gemma":0.000004352979,"domain_scores_codex":[0.9988554,0.0002966526,0.0002873527,0.0001010344,0.0003407148,0.0001189097],"domain_scores_gemma":[0.9972925,0.0006329605,0.0004437164,0.0009772425,0.000618114,0.00003542396],"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.00170752,0.001108595,0.002382813,0.0006507729,0.001000191,0.00005173005,0.005546198,0.180568,0.07318074,0.4529854,0.1388438,0.1419742],"study_design_scores_gemma":[0.003748237,0.002039842,0.02707232,0.001168007,0.0001776041,0.003711649,0.0007674047,0.382921,0.116111,0.3763515,0.0852822,0.0006492289],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.2362527,0.001548801,0.7102529,0.04441089,0.005907762,0.001218857,0.00003794976,0.0000628133,0.0003073487],"genre_scores_gemma":[0.1321184,0.000007888131,0.8671897,0.0001405594,0.0002586952,0.00002406404,0.00000140402,0.000008014844,0.0002512869],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.202353,"threshold_uncertainty_score":0.2536416,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02423893025548463,"score_gpt":0.2867847053904783,"score_spread":0.2625457751349937,"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."}}