Model Checking Systems and Specifications with Parameterized Atomic Propositions
================================================================================

In classical LTL model checking, both the system and the specification
are over a finite set of atomic propositions.  We present a natural
extension of this model, in which the atomic propositions are
parameterized by variables ranging over some (possibly infinite)
domain. For example, by parameterizing the atomic propositions send
and receive by a variable $x$ ranging over possible messages, the
specification $G(send.x -> F receive.x)$ specifies that not only each
send signal is followed by a receive signal, but also that the content
of the received message agrees with the content of the one sent.

Our extended setting consists of {\em Variable LTL} (VLTL) -- a
specification formalism that extends LTL with atomic propositions
parameterized by variables, and {\em abstract systems} -- systems in
which atomic propositions may be parameterized by variables.  We study
the model-checking problem in this setting. We show that while the
general setting is undecidable, some useful special cases are
decidable.  In particular, for fragments of VLTL that restrict the
quantification over the variables, the model checking is
PSPACE-complete, and thus is not harder than the LTL model checking
problem.  The latter result conveys the strength and advantage of our
setting.