{"id":"W2616942550","doi":"10.1109/syscon.2017.7934785","title":"Formalization of Birth-Death and IID processes in higher-order logic","year":2017,"lang":"en","type":"article","venue":"2017 Annual IEEE International Systems Conference (SysCon)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Mathematical proof; Theoretical computer science; Process calculus; Markov process; State space; Markov chain; Scalability; Model checking; Formal methods; Probabilistic logic; Algorithm; Mathematics; Programming language; Artificial intelligence; Machine learning","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.0006786395,0.0001814947,0.0002795389,0.0002089029,0.0001713683,0.0005161666,0.001689923,0.0001281025,0.00001952627],"category_scores_gemma":[0.0005216889,0.0001653215,0.00002720352,0.0001146468,0.0001516112,0.00304674,0.000229116,0.0001269307,0.00002234183],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005970013,"about_ca_system_score_gemma":0.0001916243,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0005781776,"about_ca_topic_score_gemma":0.00007712261,"domain_scores_codex":[0.9983045,0.00009451845,0.0005337815,0.0004114225,0.000433723,0.0002220947],"domain_scores_gemma":[0.9971274,0.00007252571,0.0007684262,0.0006386241,0.001324452,0.00006862458],"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.00003679692,0.0001003631,0.01954268,0.0003343759,0.00004185812,0.00001113343,0.001726044,0.0002900117,0.0009868961,0.9718631,0.0001804298,0.004886327],"study_design_scores_gemma":[0.004724356,0.0009217121,0.4302466,0.00319716,0.00004107747,0.0002760523,0.001253972,0.4630213,0.01668276,0.02803888,0.04938851,0.002207573],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1343088,0.0003973527,0.8102214,0.001811146,0.00793393,0.0009540764,0.000141719,0.0001593261,0.0440722],"genre_scores_gemma":[0.9851298,0.00013051,0.01281717,0.0000460498,0.0001390358,0.00005977231,0.000008317317,0.000008795896,0.001660541],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9438242,"threshold_uncertainty_score":0.6741616,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1256810603399984,"score_gpt":0.3575524301032098,"score_spread":0.2318713697632113,"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."}}