{"id":"W7084100230","doi":"10.1109/seai65851.2025.11108853","title":"Symoblic Model Checking for Multi-Agent Systems Based on ATLE","year":2025,"lang":"en","type":"article","venue":"","topic":"Bacterial Genetics and Biotechnology","field":"Biochemistry, Genetics and Molecular Biology","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Novelis (Canada)","funders":"","keywords":"Model checking; Symbolic trajectory evaluation; Binary decision diagram; Temporal logic; Abstraction model checking; Computation tree logic; Robotics; Binary number","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.002754757,0.0008933895,0.0009691123,0.001713735,0.0009024737,0.002367927,0.001713924,0.0009120817,0.002766263],"category_scores_gemma":[0.01342952,0.0006061796,0.002205351,0.0008812035,0.002211383,0.002792197,0.002860771,0.001755967,0.0003289043],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001858941,"about_ca_system_score_gemma":0.003378237,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.008379741,"about_ca_topic_score_gemma":0.01182157,"domain_scores_codex":[0.9965521,0.001181361,0.0002443827,0.000503766,0.001141793,0.0003765786],"domain_scores_gemma":[0.9888453,0.008387303,0.0007379876,0.0009888787,0.0008776675,0.000162849],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000286561,0.0001589443,0.003578494,0.000270507,0.0001626998,0.0006185138,0.0003303488,0.8091085,0.008207949,0.138201,0.0008422896,0.03823419],"study_design_scores_gemma":[0.00002831976,0.00002699956,0.00008845971,0.00001323464,0.00002064964,0.00004756046,0.00002772842,0.9576022,0.003640795,0.03788929,0.0006053885,0.00000940356],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02900311,0.00007693147,0.9663608,0.0001960073,0.00002514688,0.00009079486,0.0002006515,0.001636392,0.002410216],"genre_scores_gemma":[0.7552372,0.0001308738,0.2415888,0.0001679166,0.00002469649,0.0002119315,0.0005920813,0.0001949123,0.001851578],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.008379741,"threshold_uncertainty_score":0.01666188,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02813526062964222,"score_gpt":0.2825577573412833,"score_spread":0.2544224967116411,"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."}}