{"id":"W2395626435","doi":"10.2168/lmcs-11(3:11)2015","title":"Abstract Model Repair","year":2015,"lang":"en","type":"article","venue":"Logical Methods in Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"McMaster University","funders":"European Social Fund; Natural Sciences and Engineering Research Council of Canada; European Commission; Athens University of Economics and Business","keywords":"Kripke structure; Model checking; Soundness; Computer science; Abstraction; Theoretical computer science; Semantics (computer science); Kripke semantics; State (computer science); Abstraction model checking; Modal logic; Algorithm; Discrete mathematics; Programming language; Modal; Mathematics; Intermediate logic; Description logic","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.01451992,0.000214016,0.0002957256,0.0003591631,0.0001409698,0.0002928126,0.003552193,0.0001202563,0.000003739606],"category_scores_gemma":[0.001428072,0.0001758796,0.00009148429,0.002467465,0.0005740674,0.001833528,0.001453765,0.0003971148,0.00004398807],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002432542,"about_ca_system_score_gemma":0.0003683762,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001168501,"about_ca_topic_score_gemma":7.47683e-7,"domain_scores_codex":[0.9963608,0.0004572345,0.0005555821,0.00111629,0.0008427352,0.0006673476],"domain_scores_gemma":[0.9973966,0.0003511308,0.0001517736,0.001414802,0.0002648396,0.0004208588],"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.000008331866,0.000146746,0.0003118053,0.000009099659,0.000001993228,0.00002360254,0.0007366003,0.0691528,0.001869623,0.3573182,0.00013511,0.5702861],"study_design_scores_gemma":[0.000168744,0.00009013025,0.005570724,0.00001310985,8.071636e-7,0.00002164219,0.000004555681,0.8619477,0.002407111,0.1293227,0.0002388464,0.000213956],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00379137,0.00005899824,0.9888821,0.000240451,0.00139387,0.000192313,3.458185e-7,0.000532905,0.004907706],"genre_scores_gemma":[0.0397356,0.000004045069,0.9593649,0.0007661947,0.00008348528,0.00002177561,1.77407e-7,0.000006571513,0.00001723932],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7927949,"threshold_uncertainty_score":0.7172163,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2222698639982402,"score_gpt":0.4436221654901364,"score_spread":0.2213523014918962,"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."}}