{"id":"W2062100393","doi":"10.1142/s021819400800391x","title":"SUPPORTING FORMAL VERIFICATION OF DIMA MULTI-AGENTS MODELS: TOWARDS A FRAMEWORK BASED ON MAUDE MODEL CHECKING","year":2008,"lang":"en","type":"article","venue":"International Journal of Software Engineering and Knowledge Engineering","topic":"Multi-Agent Systems and Negotiation","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université du Québec à Trois-Rivières","funders":"","keywords":"Computer science; Model checking; Rewriting; Programming language; Formal verification; Formal methods; Rotation formalisms in three dimensions; Temporal logic; Linear temporal logic; Software engineering; 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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004564608,0.000198857,0.000266047,0.0004768353,0.00005224277,0.00004968001,0.0005162872,0.0001007304,0.000002124581],"category_scores_gemma":[0.0004752476,0.0001966555,0.0001356464,0.0001697763,0.00001135768,0.0007679306,0.00008966778,0.0002846736,0.000001329948],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001242164,"about_ca_system_score_gemma":0.0001063566,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004256668,"about_ca_topic_score_gemma":1.899054e-7,"domain_scores_codex":[0.998449,0.00001333709,0.0006538802,0.0001909654,0.0004541324,0.0002387461],"domain_scores_gemma":[0.9988457,0.0001421282,0.0003328645,0.0001759748,0.00038507,0.0001182548],"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.00001232164,0.00008730392,0.0005673427,0.00008398648,0.00005753441,0.00001849106,0.001647663,0.9902785,0.001143333,0.001142638,0.00001644222,0.004944444],"study_design_scores_gemma":[0.0005610569,0.00004718058,0.003615718,0.0005895481,0.000008155693,0.0000682164,0.000009539486,0.9923466,0.00246788,0.00002517409,0.00008995026,0.0001709788],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.10924,0.0003364423,0.8892875,0.00002737876,0.0009419444,0.00006797438,0.000004951756,0.0000807602,0.00001310179],"genre_scores_gemma":[0.7481009,0.00005118722,0.2516533,0.00001078087,0.0001438412,0.000004572801,0.000002348447,0.0000192219,0.00001387249],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6388609,"threshold_uncertainty_score":0.8019377,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0379183716798623,"score_gpt":0.2861758163316216,"score_spread":0.2482574446517593,"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."}}