Advertisement

A Visual Editor to Support the Use of Temporal Logic for ADL Monitoring

  • A. Rugnone
  • F. Poli
  • E. Vicario
  • C. D. Nugent
  • E. Tamburini
  • C. Paggetti
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4541)

Abstract

The use of technology within the home environment has been established as an acceptable means to support independent living for elderly and disabled people. An area of particular interest within this domain relates to monitoring of Activities of Daily Living for those persons with a form of cognitive decline. In this area, specific tasks undertaken by the persons in the context of their normal day-to-day lives reveal a wealth of information to be used to customize their environment to improve their living experience. In our current work we investigate the development of models which can be used to represent, classify and monitor basic human behaviors and support observation and control of activities of daily living. In particular, in this paper we focus on the problem of automated recognition of sequences of events that may indicate critical conditions and unexpected behaviors requiring intervention and attention from caregivers. Our work is based on a formal framework developed with temporal logic used for the specification of critical sequences of patterns and a behavior checking engine for automated recognition. In addition we have also developed an approach to provide a means of interaction with user. A visual formalism for the specification of Linear Temporal Logic expressions reduces the barrier of technical complexity enabling the involvement of experts in the domain of healthcare services to interact with the system.

Keywords

Model Checking Temporal Logic Activity Daily Living  Patient Behavior Models 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Lymberis, A., de Rossi, D.: Wearable eHealth Systems for Personalised Health Management. In: State of the Art and Future Challenges, vol. 108, IOS Press, Amsterdam (2004)Google Scholar
  2. 2.
    Augusto, J.C., Nugent, C.D.: Designing Smart Homes, The Role of Artificial Intelligence. In: Augusto, J.C., Nugent, C.D. (eds.) Designing Smart Homes. LNCS (LNAI), vol. 4008, Springer, Heidelberg (2006)Google Scholar
  3. 3.
    Bauchet, J., Mayers, A.: Modelisation of adls in its environment for cognitive assistance. In: Proc. of the 3rd International Conference on Smart Homes and Health Telematic (ICOST’05), Sherbrooke, Canada, pp. 3–10. IOS Press, Amsterdam (2005)Google Scholar
  4. 4.
    Bouchard, B., Giroux, S., Bouzouane, A.: A logical approach to adl recognition for alzheimer’s patients. In: Proc. of the 4th International Conference on Smart Homes and Health Telematic (ICOST’06), pp. 1–8 (2006)Google Scholar
  5. 5.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)Google Scholar
  6. 6.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. Formal Methods in System Design 10(1), 47–71 (1997)CrossRefGoogle Scholar
  8. 8.
    Drusinsky, D., Shing, M.T.: Monitoring temporal logic specifications combined with time series constraints. J. UCS 9(11), 1261–1276 (2003)Google Scholar
  9. 9.
    Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-mac: A run-time assurance approach for java programs. Formal Methods in System Design 24(2), 129–155 (2004)zbMATHCrossRefGoogle Scholar
  10. 10.
    Naldurg, P., Sen, K., Thati, P.: A temporal logic based framework for intrusion detection. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 359–376. Springer, Heidelberg (2004)Google Scholar
  11. 11.
    Paggetti, C., Tamburini, E.: Remote management of integrated home care services: the dghome platform. In: Press, I. (ed.) From Smart Homes to Smart Care: Icost (2005), pp. 298–302 (2005)Google Scholar
  12. 12.
    Benedetti, M., Cimatti, A.: Bounded model checking for past ltl. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Lusini, M., Vicario, E.: Engineering the usability of visual formalisms: a case study in real time logics. In: Catarci, T., Costabile, M.F., Santucci, G., Tarantino, L. (eds.) AVI, pp. 114–123. ACM Press, New York (1998)CrossRefGoogle Scholar

Copyright information

© Springer Berlin Heidelberg 2007

Authors and Affiliations

  • A. Rugnone
    • 1
  • F. Poli
    • 1
  • E. Vicario
    • 1
  • C. D. Nugent
    • 2
  • E. Tamburini
    • 3
  • C. Paggetti
    • 3
  1. 1.Department of Systems and Computer Science, University of FlorenceItaly
  2. 2.Faculty of Engineering, University of Ulster at JorsanstownNorthern Ireland
  3. 3.I+ srl, FlorenceItaly

Personalised recommendations