{"id":"W3120557648","doi":"10.1142/s0129054121500106","title":"Timed Bounded Verification of Inclusion Based on Timed Bounded Discretized Language","year":2021,"lang":"en","type":"article","venue":"International Journal of Foundations of Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Polytechnique Montréal","funders":"","keywords":"Undecidable problem; Bounded function; Computer science; Decidability; Timed automaton; Automaton; Word (group theory); Discretization; Upper and lower bounds; Regular language; Discrete mathematics; Mathematics; Algorithm; Theoretical computer science","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.002220017,0.0001446152,0.0002795635,0.0008245833,0.0002455952,0.0002870779,0.003081924,0.0000550514,0.0000470261],"category_scores_gemma":[0.000906774,0.0001352252,0.0001658555,0.001280526,0.0004715043,0.001637385,0.0007424357,0.0001892134,0.00000863385],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002680593,"about_ca_system_score_gemma":0.001383759,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001235153,"about_ca_topic_score_gemma":0.000002334367,"domain_scores_codex":[0.9962121,0.0002192954,0.0009751103,0.0003306638,0.002076155,0.0001866395],"domain_scores_gemma":[0.9942418,0.0003272044,0.001283596,0.0007356452,0.003301842,0.0001098945],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003473126,0.001730235,0.0005494138,0.00005563271,0.0001661135,0.00005979685,0.005822024,0.01558876,0.3656966,0.3550938,0.0002852428,0.2546051],"study_design_scores_gemma":[0.001316899,0.0003151282,0.008459785,0.0002347397,0.00001671669,0.00008565257,0.00003951661,0.6898941,0.2899171,0.008683908,0.0008523175,0.0001841128],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.09038448,0.00003658856,0.9048935,0.001733795,0.001983073,0.0001011137,0.000006665979,0.00002302169,0.0008377648],"genre_scores_gemma":[0.5242499,0.000007014045,0.4754921,0.0001392016,0.00007850719,0.000001791581,0.000007808126,0.000004324931,0.00001937651],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6743053,"threshold_uncertainty_score":0.5727033,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0166647698265721,"score_gpt":0.3381901749490095,"score_spread":0.3215254051224374,"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."}}