Resumen

Early specification of behavior is a key activity for the formal verification of software systems. It is believed that the specification language should be able to combine linear and branching properties to describe the expected behavior of a system. Taking this into account in this work we present a tableau algorithm that translates Branching FVS specification into Büchi automata, enabling the possibility of performing behavioral synthesis, consolidating our approach in the implementation phase. A case of study in the hardware domain world is shown to illustrate our approach.