Model programs are used as high-level behavioral specifications typically representing abstract state machines. For modeling reactive systems, one uses input-output model programs, where the action vocabulary is divided between two conceptual players: the input player and the output player. The players share the action vocabulary and make moves that are labeled by actions according to their respective model programs. Conformance between the two model programs means that the output (input) player only makes output (input) moves that are allowed by the input (output) players model program. In a bounded game, the total number of moves is fixed. Here model programs use a background theory T containing linear arithmetic, sets, and tuples. We formulate the bounded game conformance checking problem, or BGC, as a theorem proving problem modulo T and analyze its complexity. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Veanes, M., & Bjørner, N. (2009). Input-output model programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5684 LNCS, pp. 322–335). https://doi.org/10.1007/978-3-642-03466-4_21
Mendeley helps you to discover research relevant for your work.