According to McCarthy and Hayes [1], a situation is "the complete state of the universe at an instance of time". In situation calculus, describing a dynamic domain involves determining the actions agents can take and the fluents needed to represent the changes that occur in the environment. Fluents are properties of the world that may vary throughout time. They are expressed as predicates, and their truth value depends on the context. For example, at (robot, location) might represent the location of a robot. Actions are atomic operations that can alter the condition of the world. They are expressed as predicate words, with arguments corresponding to the entities participating in the action. For example, move (robot, location) may denote the activity of moving a robot to a specified area. Situations depict the status of the world at various moments in time. They are commonly written as terms with S0 describing the original situation and do (a, s) signifying the situation created by executing action a in situation s.

In the simplest version of the situation calculus, each action is described by two axioms:

I. The possibility axiom: the possibility axiom deals with the notion of whether an action is possible to execute in a given situation. This axiom specifies the conditions under which an action can be performed.

II. The effect axiom: the effect axiom specifies how the state of the world changes after acting. It describes the transition from one situation to another as a result of executing an action.

While situation calculus offers a formal and expressive basis for reasoning about actions and changes in dynamic environments, having found application in a wide variety of both theoretical and practical works [2– 10], its complexity, scalability concerns, and limits in dealing with uncertainty and constant change can present challenges in practical AI applications. Specifically, traditional situation calculus relies heavily on layered quantification and complex temporal reasoning. It can be time-consuming and inefficient when modeling and analyzing dynamic systems, particularly as their size and complexity grow.

Moreover, the Labeled Transition System (LTS)-based approach facilitates modularity and scalability, allowing complex systems to be broken down into manageable components. This modular nature supports more straightforward integration and modification, enabling the analysis to scale effectively to larger systems without introducing ambiguity. The inherent alignment of LTS models with formal verification techniques, such as model checking, further ensures that properties like safety and liveness can be rigorously verified, providing confidence in the system's behavior under various conditions.

In this paper, we propose an alternative formalism based on the LTS model to describe the basic axioms of situation calculus, which provides a powerful and versatile framework for modeling, analyzing, and reasoning about dynamic systems. Modal logic graph models inspire this model and offer clarity, formal rigor, and an intuitive graphical representation, making it easier for both humans and machines to reason. The following section provides a summary of the LTS model.

LTSs are a fundamental concept in theoretical computer science and formal methods. They provide a mathematical framework for modeling and analyzing the behavior of concurrent and reactive systems. LTSs have been successfully applied in epistemic logic [11], providing a formal and intuitive framework for representing and analyzing the knowledge and beliefs of agents as they evolve through actions and observations. They have also been effectively studied in model checking [12], [13]. In model checking, LTSs are used to depict the behavior of a system as a collection of states and transitions. These transitions are labeled with actions or events that guide the system from one state to another. By capturing the system's structure and dynamics, LTSs offer a concise yet comprehensive model for reasoning about system behavior. Let Act be the universal set of observable actions, and let τ denote a local action that is unobservable to a component's environment. An LTS M is a quadruple 〈 , , δ, 0〉 where [14]:

I. is a finite set of states.

II. ⊆ Act is the communicating alphabet of M.

III. δ ⊆ × ∪ {τ} × is a labeled transition relation.

IV. 0 ∈ is the initial state.

This paper extends the classical notion of an LTS by integrating concepts from modal logic [15]. In this vein, we define the next components [16]:

A proposition, p. A truth function, tr(p, qi), associates the truth value, ti, of p in each state, qi, where ti=Tr(p, qi). If p is a crisp proposition, ti can be either true (1) or false (0).

A target set, T(p), is a collection of "target states." A target state, qj, is one in which tj equals 1. Thus, T(p) represents the set of all states in which p is true. p defines the target set, or T(p). If qj is the target state, it fulfills T(p). Thus, T(p) ={qj|tr(p, qj) =1} (Fig. 1).

Definition 1 ([16]). Each state, qi, is connected with the set of all states, R(qi), that are accessible from qi. R(qi) is known as the reachable set of qi. Specifically, R(qi) ={qj|qj is accessible from qi} (Fig. 2).

Definition 2 ([16]). p is possible in state qi, abbreviated as possible p/qi, if the intersection of R(qi) and T(p) is not empty, that is, if there is a target state in T(p) that can be reached from qi.

Based on predicate logic, situation calculus can be difficult to use when describing dynamic system behaviors because it relies on layered quantification and complex temporal reasoning. It leads to challenges in scaling and ambiguity when depicting actions and their outcomes.

On the other hand, employing an LTS model within the situation calculus framework could offer several advantages. Firstly, the LTS model can provide a systematic and formal explanation of action sequences and their consequences, thereby improving the clarity and precision of reasoning about dynamic systems. Secondly, the LTS model allows for a straightforward examination of state transitions and action connections, making tasks like planning and verification easier within the situation calculus framework.

Furthermore, LTS approaches naturally allow for modularity and scalability. LTS facilitates system integration and change by separating complex systems into manageable components and representing them as state-transition diagrams. This modular approach enhances the ability to extend the analysis to larger systems while maintaining cohesion and clarity.

In summary, integrating an LTS model into the situation calculus framework enhances the descriptive, manageable, and verifiable nature of dynamic system behaviors. This integration surpasses the constraints of classical situation calculus by offering a more understandable, scalable, and formal framework for analyzing actions and their outcomes.

M. N. P.: Research design, Conceptualization, and Validation, Methodology, Visualization and Formal Analysis. R. K.: Computing, editing, and Validation. The authors have read and agreed to the published version of the manuscript.

Consent for publication has been obtained from the author.

No studies involving human participants or animals were performed in this research.

This research received no specific grant from funding agencies in the public, commercial, or not-for-profit sectors.

No new data were created or analyzed in this study. Data sharing does not apply to this article.

The author has no conflicts of interest to declare relevant to this article's content.

No new data were created or analyzed in this study. Data sharing does not apply to this article.