DOI : https://doi.org/10.18517/ijaseit.6.6.1470

Formal Analysis of an Agent Support Model for Behaviour Change Intervention

Ojeniyi Adegoke (1), Azizi Ab Aziz (2), Yuhanis Yusof (3)
(1) Human Centred Computing Research Laboratory (HCC), School of Computing (SOC), Universiti Utara Malaysia (UUM), 0610 Sintok, Malaysia
(2) Human Centred Computing Research Laboratory (HCC), School of Computing (SOC), Universiti Utara Malaysia (UUM), 0610 Sintok, Malaysia
(3) Human Centred Computing Research Laboratory (HCC), School of Computing (SOC), Universiti Utara Malaysia (UUM), 0610 Sintok, Malaysia
Fulltext View | Download
How to cite (IJASEIT) :
Adegoke, Ojeniyi, et al. “Formal Analysis of an Agent Support Model for Behaviour Change Intervention”. International Journal on Advanced Science, Engineering and Information Technology, vol. 6, no. 6, Dec. 2016, pp. 1074-80, doi:10.18517/ijaseit.6.6.1470.
Citation Format :
Agent applications have been widely used in behaviour change intervention nowadays. This is due to the four features of agents: proactive, reactivity, social ability and autonomy.  However, psychological reactance is one of the major limiting causes of agent interventions. Although, many studies have investigated into both psychological reactance and behaviour change nevertheless how reactive intervention can be supported to obtain an improved behaviour change intervention is still lacking in most previous studies. Therefore, this paper describes the formal analysis of agent support model for behaviour change intervention. The analysis made use of two widely accepted approaches in agent formal evaluation namely mathematical analysis and automated verification. The mathematical analysis examined the correctness of the formal model representation and formalization that aimed to ensure that all syntax and semantic representations used in the formal model is consistent. The mathematical analysis used equilibrium property to explore the formal model consistency. Likewise, automated verification depicts the checking of the model properties against its specifications and theoretical traces.  The automated verification used Temporal Trace Language (TTL), which verifies the model properties and states against generated traces. The paper presents an agent support model that allows building agent-based software and applications that deflect psychological reactance and enhance an improved behavioural change intervention.
Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
    2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
    3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).