Complexity of the Satisfiability Problem for a Class of Propositional Schemata

Iterated schemata allow to define infinite languages of propositional formulae through formulae patterns. Formally, schemata extend propositional logic with new (generalized) connectives like e.g. Lambda(n)(i=1), and boolean OR(n)(i=1) where n is a parameter. With these connectives the new logic includes formulae such as Lambda(n)(i=1) (atoms are of the form P-1, Pi+5, P-n, ... ). The satisfiability problem for such a schema S is: "Are all the formulae denoted by S valid (or satisfiable)?" which is undecidable [2]. In this paper we focus on a specific class of schemata for which this problem is decidable: regular schemata. We define an automata-based procedure, called schAuT, solving the satisfiability problem for such schemata. schAuT has many advantages over procedures in [2,11: it is more intuitive, more concise, it allows to make use of classical results on finite automata and it is tuned for an efficient treatment of regular schemata. We show that the satisfiability problem for regular schemata is in 2-EXPTIME and that this bound is tight for our decision procedure.