{"id":"W2127990882","doi":"10.1109/acsd.2006.18","title":"On-the-fly TCTL model checking for Time Petri Nets using state class graphs","year":2006,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"Polytechnique Montréal","funders":"","keywords":"Petri net; Decidability; Model checking; Computer science; Abstraction; State (computer science); Bounded function; Finite-state machine; Property (philosophy); Class (philosophy); Deadlock; Automaton; Theoretical computer science; Algorithm; Distributed computing; Mathematics; Artificial intelligence","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001945913,0.001109194,0.0008922227,0.0008730316,0.0007477375,0.001571534,0.001696505,0.0008249442,0.002192985],"category_scores_gemma":[0.009460491,0.0006110351,0.001892616,0.0005385081,0.001763529,0.003589449,0.001337566,0.001474805,0.0002546005],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002026131,"about_ca_system_score_gemma":0.003545435,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01797094,"about_ca_topic_score_gemma":0.02526752,"domain_scores_codex":[0.9973104,0.0008632198,0.000145455,0.0004425088,0.0009203424,0.0003181216],"domain_scores_gemma":[0.9871833,0.009333836,0.0009469644,0.001730511,0.0006581789,0.0001471165],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0006566648,0.000241597,0.005485946,0.0004419191,0.0002259592,0.0006094972,0.0004899031,0.7639799,0.04201087,0.07076989,0.001728267,0.1133595],"study_design_scores_gemma":[0.00005489689,0.00004160771,0.0001310227,0.00001625278,0.00003279372,0.00005278602,0.00002004951,0.9677278,0.01427143,0.01704754,0.0005921445,0.00001175216],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05576487,0.00006815468,0.9388562,0.0001221355,0.00002295996,0.0001168308,0.0001910707,0.003772022,0.00108576],"genre_scores_gemma":[0.7406991,0.0001447306,0.2564703,0.0001141727,0.00002441898,0.0002814554,0.0004906034,0.0006188789,0.001156265],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01797094,"threshold_uncertainty_score":0.03573269,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05047877643729652,"score_gpt":0.2959950325073843,"score_spread":0.2455162560700878,"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."}}