Abstract
Multi-Valued Model Checking IoT and Intelligent Systems with Trust and
Commitment Protocols
Ghalya Alwhishi, Ph.D.
Concordia University, 2024
In the era of connectivity, numerous domains utilize multi-sensor Internet of Things
(IoT) and Intelligent Systems (IS) applications, which involve complex interactions among
numerous components in open environments. This complexity challenges the verification of
these systems’ reliability and efficiency. This study pioneers the verification of IoT applications
and intelligent systems within multi-source data environments, employing multi-agent
commitment and trust protocols, particularly in uncertain and inconsistent settings.
Our research introduces efficient frameworks to model and verify these systems, incorporating
commitment and trust protocols in settings characterized by uncertainty and
inconsistency. We extend existing logics of commitment CTLcc and CTLc and the logic of
trust TCTL to multi-valued cases for reasoning about uncertainty and inconsistency. We
introduce 3v-CTLc and 3v-CTLcc, three-valued logics of commitment for reasoning about
uncertainty, and 4v-CTLc and 4v-CTLcc, four-valued logics of commitment for reasoning
about inconsistency. In the context of trust, we introduce 3v-TCTL and 4v-TCTL, multivalued
logics for reasoning about uncertainty and inconsistency over systems with trust
protocols.
To address the complexity and time needed for developing direct algorithms, coupled
with the scarcity of multi-valued model checking tools, we developed reduction algorithms.
These algorithms transform the introduced multi-valued logics of commitment and trust
into their classical case or into CTL, facilitating interaction with efficient model checkers
such as MCMAS+ and MCMASt, and NuSMV, respectively. To demonstrate the practicality and applicability of the tool in real settings, we presented
and reported experimental results over multiple IoT and IS applications in healthcare,
finance, and smart buildings. Our findings indicate that the proposed approaches and the
MV-Checker tool are highly efficient and scalable, providing accurate results under varying
conditions.