Such systems include telecommunication protocols, telephone switches, air-traffic controllers, circuits, and many more. The goal of formal reasoning is to achieve systems with provably correct behaviour. The task of formal reasoning is to specify systems and properties of systems as mathematical objects and to supply methodologies and techniques supporting formal proofs of properties of these. Numerous semantic formalisms such as synchronisation trees, event structures, transition systems, temporal logics, Petri nets, and process algebras, to mention a few, have been proposed for the specification of reactive systems. In particular, formalisms vary in the sort of reasoning methodologies they support and encourage.
Some methods have little practical pertinence, others have more.
Some methods are decidable, others are not.