{"id":"W2028415656","doi":"10.5555/380921.380927","title":"Model-checking infinite state-space systems with fine-grained abstractions using SPIN","year":2001,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":54,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Model checking; Abstraction model checking; Automaton; Computer science; Class (philosophy); State (computer science); State space; Theoretical computer science; Finite-state machine; Temporal logic; Finite state; Transition system; Algorithm; Mathematics; Artificial intelligence","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":[],"consensus_categories":[],"category_scores_codex":[0.0004569462,0.0001439092,0.0001397898,0.000159837,0.0001819625,0.0002662847,0.0003932087,0.00005059198,0.000007143705],"category_scores_gemma":[0.00003911253,0.0001191367,0.00002961985,0.000541554,0.00003679355,0.001110535,0.00007709242,0.0001549943,0.00002906127],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00009826811,"about_ca_system_score_gemma":0.00009764613,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000328007,"about_ca_topic_score_gemma":0.0000507575,"domain_scores_codex":[0.9987921,0.00005809386,0.0002645444,0.000311983,0.0002819191,0.0002913798],"domain_scores_gemma":[0.9989586,0.00004968022,0.000163787,0.0005958788,0.0001441751,0.00008784977],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001138644,0.00003240079,0.0004412421,0.0000165338,0.00001349216,0.00001000398,0.0004277302,0.9198581,0.003399373,0.07284621,0.0000455254,0.002897986],"study_design_scores_gemma":[0.0001604393,0.0000379095,0.0005519262,0.00003269899,0.000005014209,0.00008284645,0.00005935536,0.9966222,0.001035847,0.0005464483,0.0006873225,0.000177962],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.09359863,0.00002073213,0.8986446,0.0001343053,0.0002027947,0.0001851728,0.000001076024,0.0002808474,0.006931846],"genre_scores_gemma":[0.4244635,0.000004951659,0.5746776,0.00003240929,0.00002249833,0.00001004791,8.666772e-7,0.000009069756,0.0007789859],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.3308649,"threshold_uncertainty_score":0.4858252,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09034987645924034,"score_gpt":0.3284759471626646,"score_spread":0.2381260707034243,"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."}}