{"id":"W4226254196","doi":"10.23919/acc53348.2022.9867253","title":"Sufficient Conditions for Robust Probabilistic Reach-Avoid-Stay Specifications using Stochastic Lyapunov-Barrier Functions","year":2022,"lang":"en","type":"article","venue":"2022 American Control Conference (ACC)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":8,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Lyapunov function; Soundness; Probabilistic logic; Lyapunov optimization; Robustness (evolution); Computer science; Dynamical systems theory; Control theory (sociology); Lyapunov redesign; Mathematical optimization; Robust control; Lyapunov equation; Control-Lyapunov function; Lyapunov stability; Control system; Mathematics; Lyapunov exponent; Control (management); Engineering; Nonlinear system; Artificial intelligence","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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow","sts"],"consensus_categories":[],"category_scores_codex":[0.001235031,0.0003636691,0.0005274135,0.0004499227,0.002018515,0.0003035166,0.001559242,0.00004904479,0.0005901775],"category_scores_gemma":[0.0009570143,0.0004071294,0.0002330372,0.001701908,0.0005910483,0.0005120521,0.0003473999,0.0005532693,0.00003518341],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0007553659,"about_ca_system_score_gemma":0.001027369,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001958627,"about_ca_topic_score_gemma":0.00003624875,"domain_scores_codex":[0.9960442,0.0006620227,0.0007563916,0.001084966,0.0007048355,0.000747583],"domain_scores_gemma":[0.9960445,0.0008029058,0.0007142041,0.001528773,0.0006444743,0.0002651396],"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.0001575044,0.000758283,0.0001782623,0.00003312653,0.0001646374,0.000005844782,0.00171416,0.3675091,0.01643843,0.5982735,0.001764639,0.01300249],"study_design_scores_gemma":[0.000855115,0.0004497156,0.0009163655,0.00001081678,0.0001155749,0.00004195978,0.002422212,0.9860687,0.00005285555,0.002488457,0.00606955,0.0005087151],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01137016,0.0000561052,0.9822091,0.001044482,0.001171729,0.001985475,0.00111086,0.0003625715,0.0006894956],"genre_scores_gemma":[0.8580657,0.000002644813,0.1378518,0.0004735726,0.000134426,0.002664808,0.000154233,0.00004295579,0.0006098824],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8466955,"threshold_uncertainty_score":0.9998381,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09211056549534345,"score_gpt":0.3022589371722201,"score_spread":0.2101483716768767,"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."}}