This is related to my academic project

An extended finite state machine is a tuple $SM=(I,S,T)$ (simplified):

  • $I$ is the set of identifiers and it's divided into two sets Inputs and outputs, for simplification we will just consider boolean variables. Let $\sigma$ be the evaluation function $\sigma :I \to \{0,1\}$ which associate to very identifier its value, And let $\Sigma$ be the set of all evaluations.
  • $S$ is the set of states
  • $T\subseteq S\times S \times G\times A$ the set of transitions, a transition $t=(s_1,s_2,g,a)$ means :

    • $s_1$ the source state
    • $s_2$ the target state
    • $g$ the guard,which is usual expressed in the guard language and here we can just consider it as its semantic $g:\Sigma \to \{0,1\}$ where $g(\sigma)$ is an element of $\{0,1\}$.

    • $a$ is usually expressed in the action language, and we will here identify it with its semantic $a:\Sigma \to \Sigma $ where $f(\sigma)$ is another evaluation function.

Now a configuration of the state machine $SM$ is a tuple $(s_i,\sigma)$ where $s_i$ is the current state and the $\sigma$ the current evaluation function. A run of the machine is : $$(\sigma_0,s_0)\to(\sigma_1,s_{1})\to (\sigma_2,s_2)\to \cdots (\sigma_k,s_k)\to(\sigma_{k+1},s_{k+1})\to \cdots $$ where for every $k$ we have $(s_k,s_{k+1},g,a)$ is a transition and $g(\sigma_k)=1$ (meaning true) and $a(\sigma_k)=\sigma_{k+1}$

Example of action : we denote an action by $Rep(a)=[e_1,\cdots,e_n] $ where $e_i$ is a boolean expression over the variables in $I=[o_1,\cdots,o_n,i_1,\cdots ,i_k]$ where $i_j$ are the inputs of the system and are determined by the environment. And from this representation of the action we can have $a(\sigma)(x)=e_j(\sigma) $ if $x=o_j$ and $a(\sigma)(x)=i_j$ if $x=i_j$

The guards are represented by expressions over the set of the variables $I$

What I am able to do : I was able to generate some boolean expressions that are valid or satisfiable using either well known examples, or using the threshold density of boolean formulas. Hence I am able to generate the guards and the actions (which are random, and have some properties like satisfiable or valid)

Question : how could I generate a random Extended State machine with the property that: Every state is reachable and every transition can be executed

you can use that fact that I am able to generate a formula that evaluates to $1$ or $0$ and I can generate a satisfiable or unsatisfiable formula

Any other ideas to do tests with Extended State Machines? Thanks

Edit 29/04/2016

As my question is either not very clear or difficult; I have an alternative question:

Question 2: what are some well known random Extended State Machines for which every state is reachable.

The purpose of my project is to test the efficiency of an algorithm

  • $\begingroup$ I don't understand how could I improve my question? $\endgroup$
    – Elaqqad
    Commented Apr 5, 2016 at 14:44
  • $\begingroup$ Are you still interested in this question, or did you find a solution to it? I am interested in a similar problem. $\endgroup$
    – Konchog
    Commented Jul 9, 2020 at 9:38
  • 1
    $\begingroup$ Sorry, It has been years ago, and if I remember correctly, I did not succeed in finding a solution $\endgroup$
    – Elaqqad
    Commented Jul 9, 2020 at 21:12

1 Answer 1


You can generate a random automaton naively (i.e., every state sends a directed edge uniformly at random to every other state, including itself) and then remove the unreachable states. If you start with $n$ states, you will end up with roughly $cn$ states (where $c$ is explicitly computable), and this is tighly concentrated: https://dl.dropboxusercontent.com/u/3198145/rand-dfa.pdf

Thus, if your goal is $n$ states, start with, say, $n/c$ states, generate a random automaton, and remove unreachable states. Note that this process does not sample uniformly from all $n$-state automata, but you didn't ask for a uniform distribution. See also references in that linked paper for generating random automata with various properties.

  • $\begingroup$ Thank you for your answer. What I am asking for is slightly different than "classical automaton" of finite state machines; It's Extended finite state machine and for this kind of automaton we can not directly test reachability because it's a difficult problem and it produces Space State Explosion. I am not demanding uniform distribution but only covering a large space and if there are some well known examples of EFSM I am very interested. Notice also that the number of states is expected to be not very large ( approximately 100) $\endgroup$
    – Elaqqad
    Commented May 2, 2016 at 6:41
  • $\begingroup$ I see. If reachability is a hard problem then indeed my proposed solution doesn't work. $\endgroup$
    – Aryeh
    Commented May 2, 2016 at 7:08
  • $\begingroup$ Unfortunately yes, and what I am thinking of is using some well defined examples and parametrize them like logic circuits or counters. Another idea is to extract them from existing programs. But I don't really know if any of this will work $\endgroup$
    – Elaqqad
    Commented May 2, 2016 at 7:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.