{"id":"W2016818970","doi":"10.1007/s11390-013-1324-6","title":"Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL","year":2013,"lang":"en","type":"article","venue":"Journal of Computer Science and Technology","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":14,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Markov chain; Theoretical computer science; Markov model; Markov property; Markov process; Variable-order Markov model; Formal verification; HOL; Probabilistic logic; Algorithm; Formal methods; Continuous-time Markov chain; Mathematics; Artificial intelligence; Machine learning; Programming language","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002203257,0.0001242989,0.0002484955,0.001301156,0.0001662999,0.0002877387,0.001802376,0.00008559947,0.000004105442],"category_scores_gemma":[0.0003064834,0.0000992176,0.00003132841,0.002076129,0.0005419878,0.003533508,0.0006753877,0.0003756295,0.0000156971],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00007365608,"about_ca_system_score_gemma":0.0001933269,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000006602358,"about_ca_topic_score_gemma":0.000001007959,"domain_scores_codex":[0.9982944,0.00005030914,0.0004871288,0.0002709398,0.0004296442,0.0004676154],"domain_scores_gemma":[0.9985511,0.00007796986,0.0003811257,0.0003969735,0.000482117,0.0001107478],"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.000005895511,0.00004514427,0.001876162,0.000009494186,0.000006565292,0.0000528136,0.0006197783,0.0002903327,0.003628806,0.03780293,0.0001380006,0.9555241],"study_design_scores_gemma":[0.0003572882,0.0004771549,0.01640853,0.00009824106,0.00000210767,0.0006627041,0.00002555746,0.9643818,0.004549479,0.01238742,0.0004722355,0.0001774905],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.2872583,0.00009273518,0.7102475,0.001814692,0.0002916387,0.0001020197,1.996042e-7,0.00004397322,0.0001489199],"genre_scores_gemma":[0.4593152,0.00003650045,0.5404476,0.0001423806,0.00003139153,0.000003819474,4.650921e-8,0.000003157467,0.00001992126],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9640915,"threshold_uncertainty_score":0.4045976,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.007466908350015211,"score_gpt":0.2520141899348308,"score_spread":0.2445472815848156,"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."}}