Search

Abstract: Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations. [Copyright &y& Elsevier]

Abstract: It is known that deterministic finite automata (DFAs) can be algorithmically minimized, i.e., a DFA can be converted to an equivalent DFA which has a minimal number of states. The minimization can be done efficiently (in: Z. Kohavi (Ed.), Theory of Machines and Computations, Academic Press, New York, 1971, pp. 189–196). On the other hand, it is known that unambiguous finite automata and nondeterministic finite automata can be algorithmically minimized too, but their minimization problems turn out to be -complete and -complete, respectively (SIAM J. Comput. 22(6) (1993) 1117–1141). In this paper, the time complexity of the minimization problem for two restricted types of finite automata is investigated. These automata are nearly deterministic, since they only allow a small amount of nondeterminism to be used. The main result is that the minimization problems for these models are computationally hard, namely -complete. Hence, even the slightest extension of the deterministic model towards a nondeterministic one, e.g., allowing at most one nondeterministic move in every accepting computation or allowing two initial states instead of one, results in computationally intractable minimization problems. [Copyright &y& Elsevier]