{"id":"W2234078087","doi":"10.1007/978-3-642-30885-7_11","title":"Temporal Logic Model Checking in Alloy","year":2012,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":28,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"","keywords":"Computer science; Temporal logic; Transitive closure; Model checking; Description logic; Programming language; Computation tree logic; Semantics (computer science); Theoretical computer science; Transition system; Temporal logic of actions; Logic model; First-order logic; Interval temporal logic; Mathematics","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002342003,0.0009536931,0.001189564,0.001214202,0.0008772835,0.003013958,0.002375989,0.001068806,0.00542648],"category_scores_gemma":[0.006259414,0.00110755,0.0027009,0.001264254,0.002140829,0.004178439,0.001710771,0.002225974,0.000963199],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001929014,"about_ca_system_score_gemma":0.002104839,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004388578,"about_ca_topic_score_gemma":0.005072745,"domain_scores_codex":[0.9968752,0.0008825963,0.000184025,0.0003280209,0.001465629,0.000264482],"domain_scores_gemma":[0.9966896,0.002225948,0.0001452999,0.0005283298,0.0003642037,0.00004670333],"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.0002940308,0.0001045263,0.0004031894,0.0004466788,0.0001005824,0.0002880057,0.0002587319,0.1472102,0.01015287,0.7381495,0.003656829,0.09893491],"study_design_scores_gemma":[0.00007150936,0.00004961544,0.0001108358,0.0001212732,0.00008673559,0.0001374853,0.00006930732,0.3890907,0.02027443,0.5790663,0.01088681,0.00003510071],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02146191,0.0007420478,0.9539882,0.0005504196,0.0001814527,0.0001117336,0.0002059147,0.002851851,0.01990652],"genre_scores_gemma":[0.4496136,0.001058127,0.5307055,0.000344019,0.0001332008,0.0001793738,0.0006552822,0.001129096,0.01618181],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.00542648,"threshold_uncertainty_score":0.01815331,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0604905728739901,"score_gpt":0.300761211053735,"score_spread":0.2402706381797449,"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."}}