{"id":"W2491068252","doi":"10.1109/tdsc.2016.2596719","title":"Symbolic Synthesis of Timed Models with Strict 2-Phase Fault Recovery","year":2016,"lang":"en","type":"article","venue":"IEEE Transactions on Dependable and Secure Computing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"McMaster University","funders":"","keywords":"Computer science; Automaton; Timed automaton; Bisimulation; Model checking; Theoretical computer science; Time complexity; Fault model; Algorithm","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.0004832967,0.0001725744,0.0002527694,0.0002123748,0.0001990261,0.00005563667,0.000355169,0.00008834391,0.000009856511],"category_scores_gemma":[0.0000196063,0.0001195938,0.00006258654,0.0003946179,0.00005894831,0.0006835263,0.000005643831,0.0001399944,0.000006561506],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004068205,"about_ca_system_score_gemma":0.00006315469,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002776462,"about_ca_topic_score_gemma":0.000005660972,"domain_scores_codex":[0.9986192,0.000159578,0.0003081071,0.0003916555,0.0002588004,0.000262637],"domain_scores_gemma":[0.9986116,0.0005851138,0.0001599402,0.0004421132,0.0001082029,0.00009304588],"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.0001593063,0.000235915,0.000004032758,0.00005503554,0.00008182468,0.000008425459,0.0004940239,0.04164477,0.006614503,0.004167352,0.00001811996,0.9465167],"study_design_scores_gemma":[0.0008847098,0.0004276642,0.00002623309,0.0002860783,0.00003934232,0.00006948246,0.00004487787,0.7365299,0.2603775,0.000980498,0.0000678328,0.0002659611],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.08383156,0.00004038212,0.9151762,0.00007329884,0.0001809074,0.0001560458,0.000016224,0.0001169843,0.000408421],"genre_scores_gemma":[0.7915251,0.00005225695,0.2083103,0.00002543284,0.00001492699,0.000008667465,2.077119e-7,0.00001208174,0.00005099019],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9462507,"threshold_uncertainty_score":0.4876894,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02182807377864902,"score_gpt":0.2616526338298034,"score_spread":0.2398245600511544,"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."}}