Document Open Access Logo

Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking

Authors Dario Della Monica, David de Frutos-Escrig, Angelo Montanari, Aniello Murano, Guido Sciavicco

PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.11.pdf
  • Filesize: 0.59 MB
  • 18 pages

Document Identifiers

Author Details

Dario Della Monica
David de Frutos-Escrig
Angelo Montanari
Aniello Murano
Guido Sciavicco

Cite As Get BibTex

Dario Della Monica, David de Frutos-Escrig, Angelo Montanari, Aniello Murano, and Guido Sciavicco. Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.TIME.2017.11

Abstract

The problem of temporal dataset evaluation consists in establishing to what extent a set of temporal data (histories) complies with a given temporal condition. It presents a strong resemblance with the problem of model checking enhanced with the ability of rating the compliance degree of a model against a formula. In this paper, we solve the temporal dataset evaluation problem by suitably combining the outcomes of model checking an interval temporal logic formula against sets of histories (finite interval models), possibly taking into account domain-dependent measures/criteria, like, for instance, sensitivity, specificity, and accuracy. From a technical point of view, the main contribution of the paper is a (deterministic) polynomial time algorithm for interval temporal logic model checking over finite interval models. To the best of our knowledge, this is the first application of a (truly) interval temporal logic model checking in the area of temporal databases and data mining rather than in the formal verification setting.

Subject Classification

Keywords
  • Dataset Evaluation
  • Temporal Databases
  • Model Checking
  • Interval Temporal Logics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and Guido Sciavicco. On the expressiveness of the interval logic of Allen’s relations over finite and discrete linear orders. In Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA), volume 8761 of LNAI, pages 267-281, 2014. Google Scholar
  2. J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. Google Scholar
  3. P. Balbiani, V. Goranko, and G. Sciavicco. Two sorted point-interval temporal logic. In Proc. of the 7th Workshop on Methods for Modalities (M4M), volume 278 of ENTCS, pages 31-45. Springer, 2011. Google Scholar
  4. M. H. Böhlen, J. Gamper, and C. S. Jensen. How would you like to aggregate your temporal data? In Proc. of the 13th International Symposium on Temporal Representation and Reasoning (TIME), pages 121-136. IEEE Computer Society, 2006. Google Scholar
  5. A. Bottrighi, L. Giordano, G. Molino, S. Montani, P. Terenziani, and M. Torchio. Adopting model checking techniques for clinical guidelines verification. Artificial Intelligence in Medicine, 48(1):1-19, 2010. Google Scholar
  6. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval temporal logic model checking: The border between good and bad HS fragments. In Proc. of the 8th International Joint Conference on Automated Reasoning (IJCAR), volume 9706 of LNCS, pages 389-405. Springer, 2016. Google Scholar
  7. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval vs. point temporal logic model checking: an expressiveness comparison. In Proc. of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS ), volume 65 of LIPIcs, pages 26:1-26:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.26.
  8. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Model checking the logic of allen’s relations meets and started-by is p^np-complete. In Proc. of the 7th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), volume 226 of EPTCS, pages 76-90, 2016. Google Scholar
  9. A. Chaves, M. Vellasco, and R. Tanscheit. Fuzzy rules extraction from support vector machines for multi-class classification. Neural Computing and Applications, 22(7-8):1571-1580, 2013. Google Scholar
  10. Jan Chomicki, David Toman, and Michael H. Böhlen. Querying atsql databases with temporal logic. ACM Trans. Database Syst., 26(2):145-178, June 2001. URL: http://dx.doi.org/10.1145/383891.383892.
  11. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2002. Google Scholar
  12. C. Combi and A. Montanari. Data models with multiple temporal dimensions: Completing the picture. In Proc. of the 13th International Conference on Advanced Information Systems Engineering (CAiSE), volume 2068 of LNCS, pages 187-202. Springer, 2001. Google Scholar
  13. C. Combi and P. Sala. Mining approximate interval-based temporal dependencies. Acta Informatica, 53(6-8):547-585, 2016. Google Scholar
  14. K. Deb. Multi-objective optimization using evolutionary algorithms. Wiley, London, UK, 2001. Google Scholar
  15. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B: formal models and semantics, pages 995-1072. Elsevier MIT Press, 1990. Google Scholar
  16. V. Goranko and M. Otto. Model theory of modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 249-329. Elsevier, 2007. Google Scholar
  17. J. Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935-962, 1991. Google Scholar
  18. Y. Hayashi, S. Nakano, and S. Fujisawa. Use of the recursive-rule extraction algorithm with continuous attributes to improve diagnostic accuracy in thyroid disease. Informatics in Medicine Unlocked, 1:1-8, 2015. Google Scholar
  19. F. Jiménez, G. Sánchez, and J. M. Juárez. Multi-objective evolutionary algorithms for fuzzy classification in survival prediction. Artificial Intelligence in Medicine, 60(3):197-219, 2014. Google Scholar
  20. V. Khatri, S. Ram, R. T. Snodgrass, and P. Terenziani. Capturing telic/atelic temporal data semantics: Generalizing conventional conceptual models. IEEE Trans. Knowl. Data Eng, 26(3):528-548, 2014. Google Scholar
  21. K. Kulkarni and J. E. Michels. Temporal features in SQL:2011. ACM SIGMOD Record, 41(3):34-43, 2012. Google Scholar
  22. S. le Cessie and J. C. van Houwelingen. Ridge estimators in logistic regression. Applied Statistics, 41(1):191-201, 1992. Google Scholar
  23. L. Liu and M. T. Özsu, editors. Encyclopedia of Database Systems. Springer NY, 2nd edition, 2017. Google Scholar
  24. A. Lomuscio and J. Michaliszyn. An epistemic halpern-shoham logic. In Proc. of the 23rd International Joint Conference on Artificial Intelligence (IJCAI), pages 1010-1016, 2013. Google Scholar
  25. A. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class of EHS specifications. In Proc. of the 21st European Conference on Artificial Intelligence (ECAI), pages 543-548, 2014. Google Scholar
  26. A. Lomuscio and J. Michaliszyn. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In Proc. of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 298-308. AAAI Press, 2016. Google Scholar
  27. N. Markey and P. Schnoebelen. Model checking a path. In Proc. of the 14th International Conference on Concurrency Theory (CONCUR), pages 251-265. Springer, 2003. Google Scholar
  28. M. Mashayekhi and R. Gras. Rule extraction from random forest: the RF+HC methods. In Proc. of the 28th Canadian Conference on Advances in Artificial Intelligence, pages 223-237, 2015. Google Scholar
  29. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. Acta Informatica, 53(6-8):587-619, 2016. Google Scholar
  30. A. Molinari, A. Montanari, and A. Peron. Complexity of ITL model checking: Some well-behaved fragments of the interval logic HS. In Proc. of the 22nd International Symposium on Temporal Representation and Reasoning (TIME), pages 90-100. IEEE Computer Society, 2015. Google Scholar
  31. A. Molinari, A. Montanari, and A. Peron. A model checking procedure for interval temporal logics based on track representatives. In Proc. of the 24th EACSL Annual Conference on Computer Science Logic (CSL), volume 41 of LIPIcs, pages 193-210, 2015. Google Scholar
  32. A. Molinari, A. Montanari, A. Peron, and P. Sala. Model checking well-behaved fragments of HS: the (almost) final picture. In Proc. of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 473-483. AAAI Press, 2016. Google Scholar
  33. A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. In Proc. of the 21st International Symposium on Temporal Representation and Reasoning (TIME), pages 59-68. IEEE Computer Society, 2014. Google Scholar
  34. A. Pnueli. The temporal logic of programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science (FOCS), pages 46-57, 1977. Google Scholar
  35. A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1):45-60, 1981. Google Scholar
  36. D. M. W. Powers. Evaluation: From precision, recall and F-measure to ROC, informedness, markedness &correlation. Journal of Machine Learning Technologies, 2(1):37-63, 2011. Google Scholar
  37. J. R. Quinlan. C45: Programs for Machine Learning. Morgan Kaufmann, 1992. Google Scholar
  38. E. Quintarelli. Model-Checking Based Data Retrieval, An Application to Semistructured and Temporal Data, volume 2917 of LNCS. Springer, 2004. Google Scholar
  39. P. Schnoebelen. The complexity of temporal logic model checking. In Proc. of the 4th Conference on Advances in Modal Logic, pages 393-436, 2002. Google Scholar
  40. R. T. Snodgrass, editor. The TSQL2 Temporal Query Language. Kluwer Academic Publishers, 1995. Google Scholar
  41. R. T. Snodgrass, I. Ahn, G. Ariav, D.S. Batory, J. Clifford, C. E. Dyreson, R. Elmasri, F. Grandi, C. S. Jensen, W. Käfer, N. Kline, K. Kulkarni, T. Y. C. Leung, N. Lorentzos, J. F. Roddick, A. Segev, M. D. Soo, and S. M. Sripada. TSQL2 language specification. SIGMOD Record, 23(1):65-86, 1994. Google Scholar
  42. A. U. Tansel, J. Clifford, S. K. Gadia, S. Jajodia, A. Segev, and R. T. Snodgrass, editors. Temporal Databases: Theory, Design, and Implementation. Benjamin/Cummings, 1993. Google Scholar
  43. M. Y. Vardi. Model checking for database theoreticians. In Proc. of the 10th International Conference on Database Theory (ICDT), volume 3363 of LNCS, pages 1-16. Springer, 2005. Google Scholar
  44. I. H. Witten, E. Frank, and M. A. Hall. Data Mining: Practical Machine Learning Tools and Techniques. Morgan Kaufmann Publishers Inc., 3rd edition, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact