python中的定时ctl模型检查包
pyTCTL的Python项目详细描述
Pytctl
用于在python中检查tctl模型的包
最初的实现使用networkx的有向图来表示kripke结构。
所提供的算法实现了连续tctl模型检查的Lepri et al.'s方法。 因此,这个包还实现了逐点tctl模型检查。
代码最初是为CREST项目开发的,但是最好将代码提取到自己的库中。
类似项目
@albertocasagrande正在开发一个类似的库,用于(未命名的)ctl/ltl/ctl*模型检查,名为pyModelChecking。
His approach shares some of the ideas of this project. However, it seems that he chooses to implement Kripke structures directly (no networking library) and adds some features that I probably won't implement (e.g. a text parser). On the other hand, as far as I can see there's only one algorithm hardcoded for each temporal logic. In comparison, I plan to add the possibility to add and choose between search heuristics.
I will keep following his project. Maybe we can merge forces once I know more clearly which path the pyTCTL project is going to take.