{"id":"W2061590884","doi":"10.1109/ase.2011.6100149","title":"Analyzing temporal properties of abstract models","year":2011,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Model checking; Computer science; Theoretical computer science; Scalability; Programming language; Abstraction model checking; Constraint (computer-aided design); Set (abstract data type); Satisfiability modulo theories; Modulo; Satisfiability; State space; 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.004771946,0.0006289515,0.000568409,0.001816875,0.0008492618,0.00269481,0.001129799,0.0009464028,0.00194446],"category_scores_gemma":[0.02593974,0.0007970519,0.001778413,0.001242206,0.00222671,0.005869814,0.001534198,0.00158772,0.0002554354],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00213215,"about_ca_system_score_gemma":0.001678149,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006003482,"about_ca_topic_score_gemma":0.005577748,"domain_scores_codex":[0.995028,0.001543865,0.0004021951,0.000655126,0.001968118,0.0004027947],"domain_scores_gemma":[0.9766073,0.01528218,0.002718699,0.003173329,0.001928738,0.0002898723],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0003591393,0.0001237085,0.01026072,0.0004532384,0.0001897924,0.0008161871,0.001351793,0.4085886,0.02135433,0.5085976,0.001084635,0.04682023],"study_design_scores_gemma":[0.00003417198,0.00005414106,0.000871702,0.00005903768,0.00007859805,0.0001027894,0.0001407127,0.7940323,0.01039795,0.1900664,0.004136744,0.00002544854],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.09906032,0.0002426152,0.8957166,0.0002884621,0.00003277993,0.0001092649,0.000375842,0.0009363687,0.003237787],"genre_scores_gemma":[0.7172964,0.0004381736,0.2779393,0.0001302927,0.00005207985,0.0003782726,0.00130358,0.0003194016,0.002142584],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006003482,"threshold_uncertainty_score":0.02523679,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1970832329505305,"score_gpt":0.285700313853644,"score_spread":0.08861708090311352,"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."}}