{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003198033,0.00107538,0.001156964,0.0009817703,0.0009833837,0.002198529,0.002747779,0.001653563,0.008033906],"category_scores_gemma":[0.01468089,0.0006589172,0.002176793,0.0007094929,0.00187202,0.005345562,0.005113959,0.003017312,0.001626026],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00152807,"about_ca_system_score_gemma":0.002084354,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002176393,"about_ca_topic_score_gemma":0.001612734,"domain_scores_codex":[0.9955314,0.001131707,0.0003620963,0.0008377679,0.001686082,0.0004510338],"domain_scores_gemma":[0.9897383,0.003118819,0.0005944559,0.005277742,0.00110127,0.00016947],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0008452788,0.0003413975,0.00374966,0.001075277,0.0002526365,0.001391844,0.001851919,0.2870034,0.04575725,0.4266694,0.01286239,0.2181996],"study_design_scores_gemma":[0.0001012383,0.0002482631,0.0004666892,0.0001718338,0.0001196192,0.0006655882,0.0005270094,0.5889522,0.0573019,0.3088368,0.04253216,0.00007669444],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0172843,0.00009771324,0.9754827,0.0003881573,0.00006859267,0.0001498962,0.0002429218,0.00339757,0.002888153],"genre_scores_gemma":[0.4361396,0.000235505,0.5538952,0.0003485638,0.00004304382,0.0002712021,0.001498005,0.0009598505,0.006608974],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.008033906,"threshold_uncertainty_score":0.02687609,"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."}}