{"id":"W2001789462","doi":"10.1109/edoc.2007.36","title":"Model Checking Data-Aware Workflow Properties with CTL-FO+","year":2007,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université du Québec à Montréal","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Workflow; Computer science; Model checking; CTL*; Context (archaeology); Web service; Theoretical computer science; Temporal logic; Programming language; Algorithm; Artificial intelligence; Database","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.001176048,0.0001110554,0.0001021302,0.00006716322,0.0001101934,0.000143451,0.001592409,0.00004631414,0.000006186975],"category_scores_gemma":[0.00004466189,0.00007416301,0.00001352217,0.0003325478,0.00005147551,0.001497109,0.0004440664,0.0001184005,0.0000306477],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003593952,"about_ca_system_score_gemma":0.00006677254,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002072615,"about_ca_topic_score_gemma":0.00003283234,"domain_scores_codex":[0.9987921,0.00002664664,0.0001910094,0.0003988789,0.0003101932,0.0002811413],"domain_scores_gemma":[0.9982985,0.00002096586,0.00006477824,0.001461192,0.00008869194,0.00006582738],"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.00009902742,0.0001653933,0.001478354,0.0000841852,0.00004962512,0.00002037068,0.002883026,0.02021802,0.004383774,0.2317012,0.001455388,0.7374616],"study_design_scores_gemma":[0.00009384889,0.00002779684,0.000381073,0.00002589455,0.000003427974,0.00001135282,0.00004764927,0.9854696,0.01255921,0.000521571,0.0007096633,0.0001489237],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004696242,0.00004268539,0.986341,0.0001606895,0.0001079357,0.0001386494,7.815202e-7,0.0002898699,0.00822217],"genre_scores_gemma":[0.3187125,0.000002334486,0.6804051,0.0001989122,0.00002971899,0.000003914301,0.000002386167,0.00000702839,0.0006381571],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9652516,"threshold_uncertainty_score":0.302428,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2004898126885454,"score_gpt":0.3280751238848738,"score_spread":0.1275853111963283,"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."}}