{"id":"W2242407529","doi":"10.1109/ase.2015.71","title":"General LTL Specification Mining (T)","year":2015,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":134,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"Natural Sciences and Engineering Research Council of Canada; Universities Space Research Association","keywords":"Computer science; Linear temporal logic; Property (philosophy); Temporal logic; Programming language; Set (abstract data type); Theoretical computer science; Formal specification; Data mining","routes":{"ca_aff":true,"ca_fund":true,"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.000545201,0.00005056536,0.00004946099,0.00005036499,0.00003097782,0.00008008419,0.0004758347,0.00002840241,0.0000122412],"category_scores_gemma":[0.0000944138,0.00004530857,0.00001532862,0.0002290788,0.00001579508,0.0005337953,0.00007960351,0.00003542585,0.0002279939],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004674317,"about_ca_system_score_gemma":0.00003846888,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008649695,"about_ca_topic_score_gemma":8.056303e-7,"domain_scores_codex":[0.9993415,0.00005587158,0.0001288731,0.0001780313,0.0001803613,0.0001153409],"domain_scores_gemma":[0.9993268,0.00001400446,0.00004742291,0.0004467397,0.00008426376,0.00008072001],"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.00000183396,0.00001571053,0.0003993488,0.000001164798,0.000001783199,7.658997e-7,0.0006886503,0.00009765005,0.001054915,0.9088497,0.007099266,0.08178918],"study_design_scores_gemma":[0.000363912,0.00009954662,0.01125912,0.000004556508,0.000002464343,0.00002915581,0.0001861877,0.8235795,0.04141846,0.01345642,0.1093141,0.0002865365],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01697363,0.00002046298,0.8991391,0.0003416298,0.0004848393,0.00004961397,9.038308e-8,0.0001790819,0.08281152],"genre_scores_gemma":[0.06274851,0.00000170262,0.9348308,0.000179979,0.0001101516,0.000006745395,0.000001150898,0.000003294039,0.002117617],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8953933,"threshold_uncertainty_score":0.2930477,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1335533269288322,"score_gpt":0.3329722697939045,"score_spread":0.1994189428650723,"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."}}