Menshawy, Mohamed El, Bentahar, Jamal, Kholy, Warda El and Laarej, Amine (2018) Model Checking Real-Time Conditional Commitment Logic using Transformation. Journal of Systems and Software . ISSN 01641212 (In Press)
Preview |
Text (application/pdf)
2MBBentahar-jsystemssoftware-2017.pdf - Accepted Version Available under License Spectrum Terms of Access. |
Official URL: http://dx.doi.org/10.1016/j.jss.2017.12.042
Abstract
A new logical language for real-time conditional commitments called RTCTLcc has been developed by extending the CTL logic with interval bounded until modalities, conditional commitment modalities, and fulfillment modalities. RTCTLcc allows us to express qualitative and quantitative commitment requirements in a convenient way. These requirements can be used to model multi-agent systems (MASs) employed in environments that react properly and timely to events occurring at time instants or within time intervals. However, the timing requirements and behaviors of MASs need an appropriate way to scale and bundle and should be carefully analyzed to ensure their correctness, especially when agents are autonomous. In this paper, we develop transformation algorithms that are fully implemented in a new Java toolkit for automatically transforming the problem of model checking RTCTLcc into the problem of model checking RTCTL (real-time CTL). The toolkit engine is built on top of the NuSMV tool, effectively used to automatically verify and analyze the correctness of real-time distributed systems. We analyzed the time and space computational complexity of the RTCTLcc model checking problem. We proved the soundness and completeness of the transformation technique and experimentally evaluated the validity of the toolkit using a set of business scenarios. Moreover, we added a capability in the toolkit to automatically scale MASs and to bundle requirements in a parametric form. We experimentally evaluated the scalability aspect of our approach using the standard ordering protocol. We further validated the approach using an industrial case study.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | Menshawy, Mohamed El and Bentahar, Jamal and Kholy, Warda El and Laarej, Amine |
| Journal or Publication: | Journal of Systems and Software |
| Date: | 2 January 2018 |
| Digital Object Identifier (DOI): | 10.1016/j.jss.2017.12.042 |
| Keywords: | Real-time; Qualitative and quantitative commitment requirements; Transformation technique; Complexity |
| ID Code: | 983378 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 04 Jan 2018 21:36 |
| Last Modified: | 02 Jan 2019 01:00 |
References:
F. Al-Saqqar, J. Bentahar, K. Sultan, W. Wan, E. Khosrowshahi Model checking temporal knowledge and commitments in multi-agent systems using reduction Simulation Modelling Practice and Theory, 51 (2015), pp. 45–68R. Alur, T. Feder, T.A. Henzinger The benefits of relaxing punctuality J. ACM, 43 (1) (1996), pp. 116–146
M. Baldoni, C. Baroglio, A.K. Chopra, M.P. Singh Composing and verifying commitment-based multiagent protocols Q. Yang, M. Wooldridge (Eds.), Proceedings of the 24th International Joint Conference on Artificial Intelligence IJCAI, AAAI Press (2015), pp. 10–17
J. Bentahar, M. El-Menshawy, H. Qu, R. Dssoulia Communicative commitments: Model checking and complexity analysis Knowledge-Based Systems, 35 (2012), pp. 21–34
F. Boniol, V. Wiels The landing gear system case study F. Boniol, VirginieWiels, Y.A. Ameur, K.-D. Schewe (Eds.), ABZ 2014 Case Study Track, Springer (2014), pp. 1–18
F. Chesani, P. Mello, M. Montali, P. Torroni Representing and monitoring social commitments using the event calculus Autonomous Agents and Multi-Agent Systems, 27 (1) (2013), pp. 85–130
A.K. Chopra, M.P. Singh Cupid: Commitments in relational algebra B. Bonet, S. Koenig (Eds.), Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press (2015), pp. 2052–2059
A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella NuSMV 2: An open source tool for symbolic model checking E. Brinksma, K.G. Larsen (Eds.), Proceedings of the 14th International Conference on CAV, Springer (2002), pp. 359–364
E. Clarke, O. Grumberg, D. Peled Model checking MIT Press (1999)
E.M. Clarke, E.A. Emerson, J. Sifakis Model checking: algorithmic verification and debugging Communications of the ACM, 52 (11) (2009), pp. 74–84
N. Desai, A. Mallya, A. Chopra, M. Singh Interaction protocols as design abstractions for business processes IEEE Transactions on Software Engineering, 31 (12) (2005), pp. 1015–1027
N. Desai, M. Singh A modular action description language for protocol composition Proceedings of the 22nd AAAI Conference on Artificial Intelligence (2007), pp. 962–967
W. El-Kholy, J. Bentahar, M. El-Menshawy, H. Qu, R. Dssouli Conditional commitments: Reasoning and model checking ACM Transaction on Software Engineering and Methodology, 24 (2014), Article 9:1–9–49
W. El-Kholy, M. El-Menshawy, J. Bentahar, H. Qu, R. Dssouli Formal specification and automatic verification of conditional commitments IEEE Intelligent Systems, 30 (2015), pp. 36–44
W. El-Kholy, M. El-Menshawy, A. Laarej, J. Bentahar, F. Al-Saqqar, R. Dssouli Real-time conditional commitment logic Q. Chen, P. Torroni, S. Villata, J.Y. Hsu, A. Omicini (Eds.), PRIMA 2015: Principles and Practice of Multi-Agent Systems, Springer (2015), pp. 547–556
M. El-Menshawy, J. Bentahar, R. Dssouli Symbolic model checking commitment protocols using reduction A. Omicini, S. Sardina, W. Vasconcelos (Eds.), DALT, Springer (2011), pp. 185–203
M. El-Menshawy, J. Bentahar, W. El-Kholy, R. Dssouli Reducing model checking commitments for agent communication to model checking ARCTL and GCTL* Autonomous Agent Multi-Agent Systems, 27 (3) (2013), pp. 375–418
M. El-Menshawy, J. Bentahar, W. El-Kholy, R. Dssouli Verifying conformance of multi-agent commitment-based protocols Expert Systems with Applications, 40 (1) (2013), pp. 122–138
M. El-Menshawy, J. Bentahar, W. El-Kholy, P. Yolum, R. Dssouli Computational logics and verification techniques of multi-agent commitments: Survey The Knowledge Engineering Review- Cambridge, 30 (5) (2015), pp. 564–606
M. El-Menshawy, J. Bentahar, H. Qu, R. Dssouli On the verification of social commitments and time L. Sonenberg, P. Stone, K. Tumer, P. Yolum (Eds.), AAMAS, IFAAMAS (2011), pp. 483–490
E.A. Emerson, A.K. Mok, A.P. Sistla, J. Srinivasan Quantitative temporal reasoning Real-Time Systems, 4 (4) (1992), pp. 331–352
R. Fagin, J. Halpern, Y. Moses, M. Vardi Reasoning about knowledge MIT Press (1995)
I. García-Magariño, G.P. Navarro A model-driven approach for constructing ambient assisted-living multi-agent systems customized for parkinson patients Journal of Systems and Software, 111 (2016), pp. 34–48
R. Koymans Specifying real-time properties with metric temporal logic Real-time Systems, 2 (1990), pp. 255–299
F. Laroussinie, P. Schnoebelen, M. Turuani On the expressivity and complexity of quantitative branching-time temporal logics Theoretical Computer Science, 297 (2003), pp. 297–315
A. Lomuscio, C. Pecheur, F. Raimondi Automatic verification of knowledge and time with nusmv IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, AAAI Press (2007), pp. 1384–1389
A.U. Mallya, P. Yolum, M.P. Singh Resolving commitments among autonomous agents F. Dignum (Ed.), ACL, Springer (2004), pp. 166–182
Y. Moy, E. Ledinot, H. Delseny, V. Wiels, B. Monate Testing or formal verification: DO-178C alternatives and industrial experience IEEE Software, 30 (3) (2013), pp. 50–57
J. Ouaknine, J. Worrell Some recent results in metric temporal logic F. Cassez, C. Jard (Eds.), Proceedings of the 6th International conference on Formal Modeling and Analysis of Timed Systems, Springer (2008), pp. 1–13
G.R. Santhanam Qualitative optimization in software engineering: A short survey Journal of Systems and Software, 111 (2016), pp. 149–156
P. Schnoebelen The complexity of temporal logic model checking Advances in Modal Logic, 4 (2002), pp. 1–44
M. Singh Semantical considerations on dialectical and practical commitments Proceedings of the 23th AAAI Conference on Artificial Intelligence (2008), pp. 176–181
P. Torroni, F. Chesani, P. Mello, M. Montali Social commitments in time: Satisfied or compensated M. Baldoni, J. Bentahar, M.B. van Riemsdijk, J. Lloyd (Eds.), DALT, Springer (2010), pp. 228–243
P. Yolum, M.P. Singh Reasoning about commitments in the event calculus: An approach for sepcifying and executing protocols Annals of Mathematics and Artificial Intelligence, 42 (1–3) (2004), pp. 227–253
Repository Staff Only: item control page
Download Statistics
Download Statistics