{"id":"W2008270704","doi":"10.4204/eptcs.85.3","title":"Measuring Progress of Probabilistic LTL Model Checking","year":2012,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"Natural Sciences and Engineering Research Council of Canada; Leverhulme Trust","keywords":"Measure (data warehouse); Probabilistic logic; Model checking; Set (abstract data type); Polynomial; Exponential function; Time complexity","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.012065,0.001780506,0.001381439,0.004789768,0.001041311,0.003309865,0.002688856,0.001126639,0.001789754],"category_scores_gemma":[0.05857009,0.001142345,0.0018016,0.002198987,0.004366253,0.009049365,0.003835412,0.003195832,0.0004657113],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.004228486,"about_ca_system_score_gemma":0.00213205,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003785335,"about_ca_topic_score_gemma":0.002591666,"domain_scores_codex":[0.9886568,0.00364445,0.0006423653,0.00168091,0.004367101,0.001008375],"domain_scores_gemma":[0.9443383,0.03856055,0.004111415,0.00779648,0.004241921,0.0009513748],"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.002162627,0.0001757657,0.009747439,0.0003504996,0.0001865077,0.0002181566,0.0008776686,0.6412268,0.01670808,0.2199029,0.001242205,0.1072014],"study_design_scores_gemma":[0.00005510399,0.0001233332,0.0004538953,0.00004218053,0.00004391376,0.00003205396,0.00003112957,0.8774025,0.01288364,0.1080717,0.0008250442,0.00003537654],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1368606,0.0004914925,0.8537482,0.0005648885,0.00008033709,0.000135631,0.0002520171,0.004204297,0.003662593],"genre_scores_gemma":[0.839862,0.0002460331,0.157688,0.00008640422,0.00006810184,0.0001932206,0.0003573033,0.0003408561,0.001158084],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.012065,"threshold_uncertainty_score":0.06380653,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02659591590787949,"score_gpt":0.2787672107818356,"score_spread":0.2521712948739561,"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."}}