{"id":"W6910401814","doi":"10.48550/arxiv.0912.1903","title":"Verifying Real-Time Systems using Explicit-time Description Methods","year":2009,"lang":"en","type":"preprint","venue":"arXiv (Cornell University)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"St. Francis Xavier University","funders":"","keywords":"Process (computing); Modularity (biology); Rotation formalisms in three dimensions; Synchronization (alternating current); Model checking; Rendezvous; Semaphore; Asynchronous communication","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002374319,0.0004983837,0.0006569262,0.0005562604,0.0003139097,0.0004316542,0.002409707,0.0006022319,0.00001980012],"category_scores_gemma":[0.000133433,0.00061959,0.0002694808,0.001022826,0.00007988152,0.001346956,0.001438245,0.0007029148,0.0001997683],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.000979475,"about_ca_system_score_gemma":0.0002034388,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00039752,"about_ca_topic_score_gemma":7.511579e-7,"domain_scores_codex":[0.9955871,0.00158637,0.0005519302,0.001528057,0.0001851286,0.0005614806],"domain_scores_gemma":[0.9963517,0.00015209,0.0007714884,0.002217881,0.0002849057,0.0002219231],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00006087174,0.0001403276,0.0002097294,0.0002997956,0.0001299925,0.0001522475,0.0004664786,0.6630404,0.05038666,0.277276,0.0001782908,0.007659161],"study_design_scores_gemma":[0.0002080985,0.00006497011,0.0002641155,0.0002116323,0.00009425684,0.00002208386,0.00004011608,0.9884641,0.001231155,0.008550175,0.0002296843,0.0006196179],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.09998372,0.00009098784,0.8936626,0.000009471779,0.00120291,0.0005177843,0.000005953884,0.0006754897,0.003851126],"genre_scores_gemma":[0.1920611,0.0001429138,0.8064204,0.00002461903,0.0001632354,0.00000210139,0.00001602501,0.00003713282,0.001132409],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.3254237,"threshold_uncertainty_score":0.9996256,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2032167767078547,"score_gpt":0.2735258106125422,"score_spread":0.07030903390468751,"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."}}