资源分类
》 资源 》论文》Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems

Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems

2019-11-11 | |  49 |   43 |   0
Abstract Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, nonuniform artifact-centric systems is undecidable. We provide a partial model checking procedure for artifact-centric systems against the universal fragment of a first-order version of the logic CTL. We obtain this result by introducing a counterpart semantics and developing an abstraction methodology operating on these structures. This enables us to generate finite abstractions of infinite artifactcentric systems, hence perform verification on abstract models.

上一篇：Exchanging OWL 2 QL Knowledge Bases Marcelo Arenas Elena Botoeva Diego Calvanese Vladislav Ryzhikov

下一篇：Reasoning about Continuous Uncertainty in the Situation Calculus

用户评价
全部评价

热门资源

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • Learning to learn...

    The move from hand-designed features to learned...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Learning to Predi...

    Much of model-based reinforcement learning invo...