Journal
ARTIFICIAL INTELLIGENCE
Volume 211, Issue -, Pages 51-74Publisher
ELSEVIER
DOI: 10.1016/j.artint.2014.02.005
Keywords
CTL model update; Model checking; Automatic synthesis
Categories
Funding
- DGAPA [PAPIIT IN113013]
Ask authors/readers for more resources
We present a nondeterministic, recursive algorithm for updating a Kripke model so as to satisfy a given formula of computation-tree logic (CTL). Recursive algorithms for model update face two dual difficulties: (1) Removing transitions from a Kripke model to satisfy a universal subformula may dissatisfy some existential subformulas. Conversely, (2) adding transitions to satisfy an existential subformula may dissatisfy some universal subformulas. To overcome these difficulties, we employ protections of the form (E, A, L), recording information about the satisfaction of subformulas previously treated by the algorithm. Intuitively, (1) E is the set of transitions that we cannot remove without compromising the satisfaction of previously treated subformulas. Conversely, (2) A is the set of transitions that we can add. Hence, update proceeds without diminishing E and without augmenting A. Finally, (3) L is a set of literals protecting the model labels. We illustrate our algorithm through several examples: Emerson and Clarke's mutual-exclusion problem, Clarke et. al.'s microwave-oven example, synchronous counters, and randomly generated models and formulas. In addition, we compare our method with other update approaches for either CTL or fragments of CTL. Lastly, we provide proofs of soundness and completeness and a complexity analysis. (C) 2014 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
Article
Computer Science, Artificial Intelligence
Extending the description logic εL with threshold concepts induced by concept measures
Franz Baader, Oliver Fernandez Gil
Summary: This article introduces the problem of using traditional logic-based knowledge representation languages in AI applications, which can lead to complex definitions and difficult reasoning. To overcome this, the article proposes a new concept constructor and utilizes graded membership functions to define the semantics. Additionally, a class of concept measures is introduced and the algorithmic properties of the corresponding logic are analyzed.
ARTIFICIAL INTELLIGENCE (2024)
Article
Computer Science, Artificial Intelligence
Pessimistic value iteration for multi-task data sharing in Offline Reinforcement Learning
Chenjia Bai, Lingxiao Wang, Jianye Hao, Zhuoran Yang, Bin Zhao, Zhen Wang, Xuelong Li
Summary: Offline Reinforcement Learning has shown promising results in learning task-specific policies. However, directly sharing datasets from other tasks exacerbates the distribution shift issue in offline RL. In this paper, we propose an uncertainty-based Multi-Task Data Sharing approach that provides a unified framework for offline RL and resolves the distribution shift problem. The experimental results show that our algorithm outperforms previous state-of-the-art methods in challenging MTDS problems.
ARTIFICIAL INTELLIGENCE (2024)
Article
Computer Science, Artificial Intelligence
Distributed web hacking by adaptive consensus-based reinforcement learning
Nemanja Ilic, Dejan Dasic, Miljan Vucetic, Aleksej Makarov, Ranko Petrovic
Summary: This paper proposes a novel adaptive consensus-based learning algorithm for automated and distributed web hacking. The algorithm aims to assist ethical hackers in conducting legitimate penetration testing and improving web security by efficiently identifying system vulnerabilities at an early stage. Through the use of interconnected intelligent agents and a decentralized communication scheme, the algorithm achieves fast convergence and outperforms existing schemes in terms of scalability and hacking times. This algorithm provides valuable insights and opportunities for system security administrators to effectively address identified shortcomings and vulnerabilities.
ARTIFICIAL INTELLIGENCE (2024)
Article
Computer Science, Artificial Intelligence
Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs
Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
Summary: This paper proposes a new approach for formally describing the requirement for statistical inference and checking the appropriate use of statistical methods in programs. The authors define a belief Hoare logic (BHL) for formalizing and reasoning about statistical beliefs acquired through hypothesis testing. Examples demonstrate the usefulness of BHL in reasoning about practical issues in hypothesis testing, while also discussing the importance of prior beliefs in acquiring statistical beliefs.
ARTIFICIAL INTELLIGENCE (2024)
Share Paper
