We propose a model-based systems engineering framework for supervisory control of
stochastic discrete-event systems with unrestricted nondeterminism. We intend to develop
the proposed framework in four phases outlined in this paper. Here, we study
in detail the first step which comprises investigation of the underlying model and development
of a corresponding notion of controllability. The model of choice is termed
Interactive Markov Chains, which is a natural semantic model for stochastic variants of
process calculi and Petri nets, and it requires a process-theoretic treatment of supervisory
control theory. To this end, we define a new behavioral preorder, termed Markovian
partial bisimulation, that captures the notion of controllability while preserving correct
stochastic behavior. We provide a sound and ground-complete axiomatic characterization
of the preorder and, based on it, we define two notion of controllability. The first notion
conforms to the traditional way of reasoning about supervision and control requirements,
whereas in the second proposal we abstract from the stochastic behavior of the system.
For the latter, we intend to separate the concerns regarding synthesis of an optimal supervisor.
The control requirements cater only for controllability, whereas we ensure that
the stochastic behavior of the supervised plant meets the performance specification by
extracting directive optimal supervisors.