{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.00230234,0.001425427,0.0006096555,0.002137168,0.0007098625,0.002904837,0.002237852,0.001202381,0.01691744],"category_scores_gemma":[0.01565026,0.0009923418,0.002840815,0.002472847,0.0009436148,0.002972472,0.001935653,0.001725013,0.009041245],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001219977,"about_ca_system_score_gemma":0.002927216,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.005064499,"about_ca_topic_score_gemma":0.004654156,"domain_scores_codex":[0.9967687,0.0005912192,0.0005406645,0.0007287835,0.001187336,0.0001833296],"domain_scores_gemma":[0.9930245,0.002733584,0.0006678364,0.002178596,0.001274354,0.0001211674],"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.0004301927,0.000198265,0.007968549,0.002026195,0.0002402883,0.001179697,0.0005501876,0.08200081,0.01657023,0.2100392,0.05543094,0.6233655],"study_design_scores_gemma":[0.0001092881,0.0001188127,0.0007448973,0.0003304377,0.0001113184,0.001243523,0.0001735815,0.6305154,0.03812143,0.20223,0.1262167,0.00008470572],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002060091,0.0001621572,0.9759631,0.0001842339,0.00002740759,0.0002683362,0.002487011,0.01495677,0.003890941],"genre_scores_gemma":[0.07608387,0.0005605441,0.9019322,0.0004472961,0.00006818705,0.0009299982,0.01089409,0.002642965,0.006440782],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01691744,"threshold_uncertainty_score":0.05659449,"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."}}