资源论文Dynamic Logic for Data-aware Systems: Decidability Results

Dynamic Logic for Data-aware Systems: Decidability Results

2019-10-29 | |  29 |   24 |   0
Abstract We introduce a first-order extension of dynamic logic (FO-DL), suitable to represent and reason about the behaviour of Data-aware Systems (DaS), which are systems whose data content is explicitly exhibited in their description. We illustrate the expressivity of the formal framework by modelling English auctions as DaS and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for DaS against FO-DL is decidable, provided some mild assumptions on the interpretation domain

上一篇:Deterministic, Strategyproof, and Fair Cake Cutting

下一篇:Epistemic-entrenchment Characterization of Parikh’s Axiom

用户评价
全部评价

热门资源

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • The Variational S...

    Unlike traditional images which do not offer in...

  • 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...