Refinement in the Presence of Unknowns

The standard theory of refinement assumes the systems/specifications/programs under consideration to be completely known: states and transitions are explicitly or implicitly given. This assumption fails to hold for systems that dynamically evolve over time, changing their composition as well as their components due to new requirements or new environmental conditions.In this paper, we study refinement for such partially known systems. In our setting, partiality refers to transitions: transitions between states may be present or not present (the standard case) as well as unknown. This third possibility is expressed by using a three-valued logic for reasoning. We define a simulation relation on such partial transition systems, and show that the simulation problem on partial transition systems can be rephrased in terms of two simulation problems on complete transition systems, employing an optimistic and a pessimistic completion.