{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003186478,0.001316328,0.001010451,0.001298395,0.0007549282,0.002030322,0.002940548,0.001302322,0.007859004],"category_scores_gemma":[0.007008271,0.00105593,0.002220989,0.001154603,0.001329162,0.003320221,0.001929715,0.002475827,0.002051435],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001087999,"about_ca_system_score_gemma":0.002702903,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002229563,"about_ca_topic_score_gemma":0.002452321,"domain_scores_codex":[0.9962669,0.001080199,0.0004194411,0.0004943644,0.001506742,0.0002323474],"domain_scores_gemma":[0.9966124,0.001612938,0.000199027,0.0008067391,0.0006921245,0.00007683747],"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.0003005975,0.0001807574,0.0006853719,0.0009584355,0.0001741587,0.0008505045,0.0005473783,0.1243492,0.03174593,0.5123084,0.01390003,0.3139993],"study_design_scores_gemma":[0.0002362475,0.00009827031,0.0001270287,0.0001628128,0.00013578,0.0007126014,0.00004695671,0.774424,0.03659616,0.09530247,0.0920366,0.0001211594],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0003845568,0.00004129887,0.9974405,0.00002967973,0.00003363237,0.00003913374,0.00004897477,0.001423489,0.0005587284],"genre_scores_gemma":[0.04559689,0.0002681228,0.9472238,0.0001698457,0.00005254886,0.0004377335,0.0005935808,0.001164462,0.004493037],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007859004,"threshold_uncertainty_score":0.02629095,"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."}}