PSL is a standard specification language(IEEE-1850) for hardware and embedded system design. The simple subset of PSL(PSLSimple) conforms to the notion of monotonic advancement of time, which in turn ensures that formulas within the subset can be simulated easily. Dynamic verifiers consider only finite executions which may be too short to assure their satisfaction to some formulas.

In this paper, we work on the theories and methods for designing dynamic verifiers for PSLSimple. We first study the formalism for the formula satisfaction strengths over finite words. Then, we explore the combinational laws of finite words with respect to strong satisfaction, weak satisfaction and strong violation. That contributes acceptance conditions for automata to recognize not just violating, but also strongly satisfying and pending words for all PSLsimple structures. In the end, we propose the Local-variable-enhanced Alternating Finite Automata( LAFA) as the run time checkers for PSLSimple. The size of a LAFA is linear to the size of its PSLSimple formula.