{"id":"W2876334621","doi":"10.24963/ijcai.2018/848","title":"SynKit: LTL Synthesis as a Service","year":2018,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":12,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Linear temporal logic; Software engineering; Program synthesis; Programming language; Software; Temporal logic; Service (business); Model checking","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.002058502,0.001592567,0.0009427269,0.001379435,0.0004860235,0.002000105,0.002200958,0.001515064,0.03499686],"category_scores_gemma":[0.00670926,0.0009333068,0.001590251,0.0007616912,0.001142212,0.002363846,0.002602506,0.00202288,0.01561243],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0007026098,"about_ca_system_score_gemma":0.001464953,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0008707005,"about_ca_topic_score_gemma":0.0008958704,"domain_scores_codex":[0.9984614,0.0004295626,0.0001796591,0.0002484083,0.0005359018,0.0001451791],"domain_scores_gemma":[0.9972133,0.00157044,0.0002142522,0.0005406277,0.0003285252,0.0001328249],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.001538634,0.0003412351,0.001913554,0.002437359,0.0003321873,0.002247878,0.00100716,0.06344321,0.07239579,0.167035,0.1813217,0.5059863],"study_design_scores_gemma":[0.0007051349,0.0002318732,0.0003706658,0.0003028334,0.0001294686,0.00109364,0.0001303476,0.4755073,0.07895726,0.1393849,0.3030159,0.0001707906],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001198157,0.0001244672,0.8542898,0.0001566264,0.00009801486,0.0001026972,0.000740048,0.1375539,0.005736376],"genre_scores_gemma":[0.1425137,0.000817865,0.7474977,0.001208398,0.0002220728,0.001368285,0.00667326,0.0753451,0.02435369],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.03499686,"threshold_uncertainty_score":0.1170762,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03124734967508945,"score_gpt":0.3074605161974025,"score_spread":0.276213166522313,"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."}}