{"id":"W2145158997","doi":"10.4204/eptcs.14.6","title":"An Efficient Explicit-time Description Method for Timed Model Checking","year":2009,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"St. Francis Xavier University","funders":"Natural Sciences and Engineering Research Council of Canada; Atlantic Canada Opportunities Agency","keywords":"Model checking; Process (computing); Rendezvous; Synchronization (alternating current); Modularity (biology); Automaton; State (computer science); Variable (mathematics); Semaphore","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.007441346,0.0002818835,0.0003068641,0.0004755076,0.0004038056,0.0006728304,0.003233,0.0001194076,0.000003299958],"category_scores_gemma":[0.0003032305,0.0002649051,0.00007928073,0.001928685,0.0003837135,0.001831307,0.0002398481,0.0003949522,0.000009578302],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006106552,"about_ca_system_score_gemma":0.0002956556,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":7.883182e-7,"about_ca_topic_score_gemma":8.769245e-8,"domain_scores_codex":[0.9960464,0.00005918654,0.000487697,0.001287144,0.0007334945,0.001386049],"domain_scores_gemma":[0.9985925,0.00009858051,0.0001652653,0.0005289553,0.0003793866,0.000235323],"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.0000280238,0.0001258493,0.000002038942,0.000006024149,0.000001287717,2.547958e-7,0.000693442,0.009448635,0.04874284,0.8851853,0.000009095104,0.05575719],"study_design_scores_gemma":[0.0002363388,0.0006839351,0.00007209963,0.00002220956,0.000003196514,0.00001810169,0.000005055825,0.6676424,0.03731676,0.2937649,0.000009954147,0.0002251094],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03762836,0.00002453473,0.9598686,0.000469519,0.0001404479,0.0006267653,4.575442e-7,0.0003422297,0.0008991605],"genre_scores_gemma":[0.4880915,0.000001419964,0.5115241,0.0002840556,0.00005272032,0.00003466929,5.016699e-7,0.00000741167,0.000003636212],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6581937,"threshold_uncertainty_score":0.9999803,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01322371411625222,"score_gpt":0.3050697146368014,"score_spread":0.2918460005205492,"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."}}