Paper Info
Title
Experimental Evaluation of Acacia-K: A Tool for Synthesis of Reactive Systems from KLTL+ Specifications
Abstract
Acacia-K is a tool that solves the synthesis problem for the positive fragment of epistemic temporal logic (KLTL). We briefly describe the implemented algorithm and our test cases. The tool is an extension of Acacia+ that solves the synthesis problem for epistemic temporal specifications where the resulting strategies need memory. To stress more the importance of such implementation, in this paper we compare Acacia-K with MCMAS-SLK, an open-source model-checker supporting the verification of interactive systems against specifications written in a variant of strategy logic under memoryless setting. The results obtained prove the feasibility of our method and represent an encouraging (and necessary) step towards developing implementable procedures for the entire logic KLTL.
Year
DOI
Venue
2018
10.1109/SYNASC.2018.00031
2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
Keywords
Field
DocType
synthesis,verification,interactive systems,epistemic temporal logics,imperfect information
Computer science,Theoretical computer science,Test case,Temporal logic,Perfect information,Reactive system
Conference
ISSN
ISBN
Citations 
2470-8801
978-1-7281-0626-7
0
PageRank 
References 
Authors
0.34
5
1
Name
Order
Citations
PageRank
Rodica Condurache101.35