 Hennessy–Milner logic

Hennessy-Milner logic is a modal logic used for specifying and reasoning about the behaviors of concurrent systems. It is particularly aimed at modeling the properties of systems that can exhibit different behaviors based on their state and the actions they can perform. The logic is named after Michael Hennessy and Robin Milner, who developed it in the context of studying process calculi, specifically for characterizing the behavior of processes in terms of their interactions and communication.