{"id":"W1770557760","doi":"","title":"A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties","year":2008,"lang":"en","type":"article","venue":"PolyPublie (École Polytechnique de Montréal)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":21,"is_retracted":false,"has_abstract":true,"ca_institutions":"Polytechnique Montréal","funders":"","keywords":"Abstraction; Petri net; Partial order reduction; Model checking; Computer science; Abstraction model checking; State space; Automaton; Time complexity; Theoretical computer science; Construct (python library); Extension (predicate logic); Reduction (mathematics); Büchi automaton; Linear temporal logic; Algorithm; State (computer science); Mathematics; Programming language; Deterministic automaton","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.001060146,0.0003996421,0.000376255,0.0006233513,0.0004465239,0.0002060382,0.001207287,0.0002062451,0.000008046703],"category_scores_gemma":[0.0003819132,0.0003882639,0.0001409755,0.001131,0.0001080513,0.0008065999,0.0004558852,0.0004921916,0.000184411],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006602771,"about_ca_system_score_gemma":0.0003616232,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001183532,"about_ca_topic_score_gemma":0.0000433496,"domain_scores_codex":[0.9968981,0.0001517203,0.0005940576,0.0007606219,0.0007422025,0.0008533529],"domain_scores_gemma":[0.9975455,0.00005684237,0.0003018595,0.001420255,0.0002739384,0.0004015536],"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.00011554,0.0002588221,0.0005544808,0.0000313662,0.00002536503,0.0000424575,0.003237078,0.9254349,0.05947476,0.002562762,0.001156496,0.007105922],"study_design_scores_gemma":[0.0002191061,0.0001105562,0.006415094,0.00004772145,0.000007944408,0.0001458461,0.00002290499,0.894284,0.09760006,0.0001424266,0.0005954189,0.0004089103],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.3000169,0.0001255187,0.6960117,0.00173881,0.0001060645,0.0007655271,0.000009270026,0.001004911,0.0002213813],"genre_scores_gemma":[0.3870594,0.00003229827,0.6100032,0.0007489492,0.00006117802,0.0002713292,0.00000540758,0.0000474423,0.001770832],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.08704257,"threshold_uncertainty_score":0.9998569,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02859817003590964,"score_gpt":0.2542420033655314,"score_spread":0.2256438333296218,"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."}}