Construction of Linear Temporal Property verification extension

by Phuc Nguyen Dinh for The Java Pathfinder Team

JPF can verify various temporal properties, yet it hasn’t supported of generic temporal property verification (LTL or CTL). Presently,LTL-translator extension has implemented; however, Buechis received are quite generic, so there haven’t been any extension to check them. Thus, user must implement a corresponding listener to each property they want to verify. Hence, I propose a JPF extension that furnishes generic support for LTL and provide simpler way of concrete temporal property verification.