## 3 Timed Interpreted Systems  
Interpreted systems (ISs) [41] were initially developed to model distributed systems. However, with the increasing interest in Multi-agent Systems [42], the concept of ISs has evolved into a formalism for modelling, for example, communication between agents. Over the years, this formalism has been successfully extended [4; 43; 44]. The formalism of TISs, as presented in [4], enhances ISs by enabling reasoning about the _discrete_ time aspects of MASs. In our work, we have extended this capability to reason about the _real-time_ aspects of MASs. The primary advantage of employing dense time semantics is that timed models with dense time allow for abstraction from the specific rate at which clocks may tick. In contrast, using discrete-time semantics results in timed models where each clock ticks and measures time in discrete units.  
The Intuition Behind Interpreted Systems, Interleaved Interpreted Systems and a Network of Timed Automata  
Timed Interpreted Systems offer a powerful and expressive framework for modelling security protocols, especially when timing is critical. They enable the detailed analysis of time-dependent behaviours and vulnerabilities, providing insights that other models might overlook. However, these advantages have significant challenges, including increased complexity, resource demands, and scalability issues.  
The previous approaches usually used timed automata to model security protocols.  
To compare our new approach to modelling and verification security protocols to the existing ones, we present the intuition behind Timed Interpreted Systems, Timed Interleaved Interpreted Systems, and Timed Automata. The main difference and the crucial one lie in action synchronisation.  
In standard interpreted systems, all agents perform actions synchronously [45]. This means that every agent in the system executes an action simultaneously at each discrete time step (often modelled as a global clock tick). The global state of the system transitions based on the combination of actions taken by all agents at that time step. The collective effect of these actions determines the system's evolution. The system progresses in synchronised time steps where each agent acts. The system considers the joint action of all agents to determine the next global state. If the agents' actions and the environment's response are deterministic, the next state is uniquely determined by the current state and the agents' actions. Agents may need to coordinate their actions, as they know other agents act simultaneously.  
In interleaved interpreted systems [45], agents perform actions asynchronously. At each time step, only one agent executes an action while the others remain idle. Thus, agents' actions are interleaved over time rather than occurring simultaneously. The global state transitions are based solely on the action of the single active agent at that time step. The system's evolution results from individual agents acting one after another in some order. The system represents all possible sequences (interleavings) of agent actions. The order in which agents act may be non-deterministic unless specified by some scheduling policy. Agents act independently without the assumption that others are acting simultaneously. Agents do not need to consider concurrent actions by others at the same time step.  
In a Network of Automata [10], multiple automata (representing agents or system components) operate concurrently. Synchronisation is achieved through explicit mechanisms, such as synchronisation labels, channels, or shared actions. Automata can perform actions independently or synchronously with other automata, depending on the synchronisation requirements. Synchronisation can be partial (involving only some automata) or full (involving all automata).