{"id":"W2603469395","doi":"10.1007/s10626-017-0243-z","title":"Augmented finite transition systems as abstractions for control synthesis","year":2017,"lang":"en","type":"article","venue":"Discrete Event Dynamic Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":47,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"Defense Advanced Research Projects Agency; National Science Foundation","keywords":"Realizability; Liveness; Preorder; Transition system; Abstraction; Computer science; Representation (politics); Class (philosophy); Temporal logic; Theoretical computer science; Mathematics; Algorithm; Discrete mathematics","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.001336417,0.0007645182,0.0008288256,0.0007479432,0.0004028875,0.001820791,0.001184598,0.0007951144,0.003531239],"category_scores_gemma":[0.003027729,0.0006127873,0.00139689,0.0006588733,0.001520927,0.001757189,0.001568518,0.002103225,0.0006183462],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006879538,"about_ca_system_score_gemma":0.001067259,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001260827,"about_ca_topic_score_gemma":0.001639841,"domain_scores_codex":[0.9987903,0.0004362371,0.00009441667,0.0002004269,0.0003557925,0.0001228437],"domain_scores_gemma":[0.997962,0.001210365,0.0001586308,0.0004836468,0.0001389778,0.0000465043],"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.0002460972,0.00006106787,0.0004147517,0.0004122645,0.0001042847,0.0002607054,0.0004296987,0.4149927,0.01521193,0.5015217,0.0007277443,0.065617],"study_design_scores_gemma":[0.00004920206,0.0001062462,0.0001189309,0.00009395777,0.00009451586,0.00006578316,0.00004769738,0.7213811,0.008325463,0.2591883,0.01050249,0.00002628215],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.006154663,0.0002074018,0.9912462,0.00002522133,0.00004154453,0.0000330451,0.00005283374,0.0005528457,0.001686288],"genre_scores_gemma":[0.5058969,0.0006082047,0.4884407,0.0000650853,0.00004828539,0.0002436879,0.0002639606,0.0001969681,0.004236386],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003531239,"threshold_uncertainty_score":0.01181322,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02022099788410862,"score_gpt":0.3220518371624749,"score_spread":0.3018308392783662,"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."}}