这里记录一下学习LTL2BA和SPIN实现LTL satisfiability checking 1. LTL satisfiability checking关注这样一类问题：对于一个系统，给定一个由线性时序逻辑（LTL）描述的性质，判断系统是否具有该性质，解决该问题的理论方法之一简单理解是将LTL性质转换为等价的Buchi自动机，再列举系统所有的运行轨迹，检验这些运行轨迹能否使得Buchi自动