This paper proposes a Hybrid Turing Machine (HTM) framework for modeling and controlling cyber-physical systems (CPS), which integrates discrete symbolic computation with continuous physical evolution. In HTM, each symbolic configuration is associated with real-valued dynamics governed by neural flow functions, and transitions are triggered by guard predicates based on system evolution. A pointer-based memory mechanism induces partial observability, which is addressed by a recurrent neural network (RNN) that encodes controller and device behavior into latent continuous states. We prove that computing the maximum total reward or synthesizing an optimal policy in HTM is incomputable, motivating an approximate control approach. To this end, we abstract HTM execution traces into a Partially Observable Markov Decision Process (POMDP) using latent discrete state clustering and RNN-based dynamic modeling. Reinforcement learning is then applied to train a policy over the latent POMDP, which is lifted back to the HTM configuration space for execution. Experimental results on a multi-UAV scheduling task show that our framework enables interpretable hybrid control and consistent decision-making under limited observability.

Cyber-Physical Systems (CPS) are the next generation of intelligent systems that integrate information control devices with physical resources. With increasingly close connections between CPS components and frequent interactions, potential defects grow exponentially, rendering the operating environment of CPS unreliable. Therefore, research on methods and theories to ensure the correctness, safety and reliability of CPS is not only an important research topic but also an inevitable challenge. In this paper, we propose a CPS modeling and verification method based on Architecture Analysis & Design Language (AADL) and process algebra to address this challenge. Due to the continuous, time-constrained, stochastic, uncertain and concurrent characteristics of CPS, this paper considers both flexibility and rigor in the modeling process. We first extend the ability of AADL to describe the multiple characteristics of CPS and propose Hybrid Probability-AADL (HP-AADL). Second, this paper introduces conditional execution, conditional interruption and probability operators into Temporal Calculus of Communication Systems (TCCS) and designs a new formal modeling language Hybrid Probability-Temporal Calculus of Communication Systems (HP-TCCS). However, HP-AADL is a semi-formal modeling language that cannot be directly used for formal verification, it cannot strictly guarantee the quality of the established CPS models, including its functional correctness and safety. Therefore, this paper proposes transformation rules from HP-AADL to HP-TCCS, which enables model checking of CPS models described in HP-AADL within HP-TCCS. Additionally, this paper designs a new formal specification language HPAT-Spatial Temporal Logic (HPAT-STL) based on Probabilistic Computation Tree Logic (PCTL) and Spatial Logic, which characterizes the temporal, probabilistic and spatial properties of CPS model. To achieve formal verification of HP-TCCS model and HPAT-STL formulas, this paper proposes a model checking algorithm HPAT-Model Checking Algorithm (HPAT-MCA). Finally, we discuss a typical CPS example to demonstrate the effectiveness of our proposed method in ensuring correct, safe and reliable CPS.

Temporal Logics are a rich variety of logical systems designed for specifying properties over time, and about events and changes in the world over time. Traditional temporal logic, however, is limited to binary outcomes true or false and lacks the capacity to specify performance properties of a system such as the maximum, minimum, or average costs between states. Current languages do not accommodate the quantification of such performance properties, especially in scenarios involving infinite execution paths where performance property like cumulative sums may fail to converge. To this end, this paper introduces a novel formal language aimed at assessing system performance, which encapsulates not only temporal dynamics but also various performance-related properties. In this study, this paper utilizes reinforcement learning techniques to compute the values of performance property formulas. Finally, in the experimental part, a formal language representation of system performance properties was implemented, and the values of the performance property formulas were computed using reinforcement learning. The effectiveness and feasibility of the proposed method were validated.

Path generation means generating a path or a set of paths so that the generated path meets specified properties or constraints. To our knowledge, generating a path with the performance evaluation value of the path within a given value interval has received scant attention. This paper subtly formulates the path generation problem as an optimization problem by designing a reasonable fitness function, adapts the Markov decision process with reward model into a weighted digraph by eliminating multiple edges and non-goal dead nodes, constructs the path by using a priority-based indirect coding scheme, and finally modifies the bat algorithm with heuristic to solve the optimization problem. Simulation experiments were carried out for different objective functions, population size, number of nodes, and interval ranges. Experimental results demonstrate the effectiveness and superiority of the proposed algorithm.

Probabilistic behavior is omnipresent in computer-controlled systems, in particular, so-called safety-critical hybrid systems, due to various reasons, like uncertain environments or fundamental properties of nature. In this paper, we extend the existing hybrid process algebra ACP[Formula: see text] with probability without sacrificing the nondeterministic choice operator. The existing approximate probabilistic bisimulation relation is fragile and not robust in the sense of being dependent on the deviation range of the transition probability. To overcome this defect, a novel approximate probabilistic bisimulation is proposed which is inspired by the idea of Probably Approximately Correct (PAC) by relaxing the constraints of transition probability deviation range. Traditional temporal logics, even probabilistic temporal logics, are expressive enough, but they are limited to producing only true or false responses, as they are still logics and not suitable for performance evaluation. To settle this problem, we present a new performance evaluation language that expands quantitative analysis from the value range of [Formula: see text] to real number to reason over probabilistic systems. After that, the corresponding algorithms for performance evaluation are given. Finally, an industrial example is given to demonstrate the effectiveness of our method.

Compositional stochastic model checking in the assume-guarantee style is a theoretically feasible way to alleviate the state explosion problem. The key for assume-guarantee reasoning is how to generate assumption. A main automated approach for assume-guarantee are based on learning assumptions. However, L*-based learning assumptions for stochastic systems produces many intermediate results which need to be recorded. To overcome this, we propose a novel learning technique based on genetic algorithm for compositional stochastic model checking of Markov decision process, which is a randomized algorithm essentially. There are no intermediate results need to be recorded in the genetic algorithm-based learning algorithm, except the encoding of the problem domain and the training set. It can reduce the space complexity largely with respect to derivation algorithms. We implement a prototype tool for it and report encouraging results.

Counterexample-guided abstraction refinement (CEGAR) is an extremely successful methodology for combating the state-space explosion problem in model checking. State-space explosion problem is more serious in the field of stochastic model checking, and it is still a challengeable problem to apply CEGAR in stochastic model checking effectively. In this paper, we formalize the problem of applying CEGAR in stochastic model checking, and propose a novel CEGAR framework for it. In our framework, the abstract model is presented by a quotient probabilistic automaton by making a set of variables or latches invisible, which can distinguish more degrees of abstraction for each variable. The counterexample is described by a diagnostic sub-model. Validating counterexample is performed on diagnostic loop paths, and the directed explicit state-space search algorithm is used for searching diagnostic loop paths. Sample learning, particle swarm optimization algorithm (PSO) and some effective heuristics are integrated for refining abstract model guided by invalid counterexample. A prototype tool is implemented for the framework, and the feasibility and efficiency are shown by some large cases.

Providing counterexample for the refutation of a property is an essential feature of model checking, if it is not the most important. However, generating counterexample in stochastic model checking needs a dedicated algorithm. It usually costs too much time and memory, and sometimes it cannot find the counterexample. What is worse, generating smallest counterexample in stochastic model checking has been proved to be NP-complete, and it is unlikely to be efficiently approximable. Although there are a few heuristic methods that are applied to the construction of the counterexample, it is usually difficult to determine the heuristic function which is critical for counterexample generating. In this paper, we present a particle swarm optimization (PSO)-based approach to generating counterexample for stochastic model checking. We define the diagnostic sub-graph as counterexample, and extend PSO algorithm with heuristic (HPSO) to generate counterexample. It adopts indirect path coding scheme to expand the scope of the search space, and employs heuristic operator to generate more effective path. The validity of our approach is illustrated by some case studies in a prototype tool. The experiments show that HPSO algorithm can significantly outperform the present algorithm for counterexample generation in stochastic model checking.

Ensuring dependability is significant in the development process of Real-Time Embedded Systems (RTESs). The dependability of a system model is usually presented by temporal and data constraints, which are ambiguous and incomplete when using semi-formal methods. Formal methods have precise semantics and strong verifiability, but few can capture the dependability features for RTESs. This paper presents Z-MARTE, an extensible modeling method combining MARTE profile and Z notation, to provide rigorous specifications towards the dependability features of RTESs. To extend the descriptive ability of Z, we design the time model, structure model and behavior model in Z-MARTE, specifying temporal and data constraints in the form of predicates. Z-MARTE can be edited and verified by the existing tools for Z. The converting from MARTE to Z-MARTE is supported by ZMT, a model transformation tool we design. A case study of a communication system is given to illustrate the modeling and verification procedure of Z-MARTE.

In this paper, we present a normal bisimulation for higher order π-calculus with unguarded choice and prove the coincidence between such normal bisimulation and context bisimulation for higher order π-calculus with unguarded choice. To achieve this aim, we introduce indexed higher order π-calculus with unguarded choice. Furthermore we present corresponding indexed bisimulations in this calculus, and prove the equivalence between indexed context bisimulation and indexed normal bisimulation. As an application of this result, we prove the equivalence between context bisimulation and normal bisimulation for higher order p-calculus with unguarded choice.

In this paper, we present a normal bisimulation for higher order pi-calculus with unguarded choice and prove the coincidence between such normal bisimulation and context bisimulation for higher order π-calculus with unguarded choice. To achieve this aim, we introduce indexed higher order π-calculus with unguarded choice. Furthermore we present corresponding indexed bisimulations in this calculus, and prove the equivalence between indexed context bisimulation and indexed normal bisimulation. As an application of this result, we prove the equivalence between context bisimulation and normal bisimulation for higher order π-calculus with unguarded choice.

In this paper, we present a higher order ambient calculus HSAP, which is a higher order extension of SAP calculus. In HSAP, we extend higher order communication capability and administrator interaction capability. Higher order communication capability means that an ambients can be send to another ambients. Administrator interaction capability means that an ambients can interact with any ambients if the password is matched. Then, we give a LTS based operational semantics for HSAP and two labelled bisimulations, called early bisimulation and late bisimulation. Early bisimulation is proved to coincide with reduction barbed congruence. Furthermore, we present late bisimulation, quasi late bisimulation, concise quasi late bisimulation and quasi normal bisimulation for HSAP and study the relation between these bisimulations. Finally, we study the expressiveness of HSAP.

In this paper, we propose open bisimulations for open processes in higher order π-calculus. The equivalence of open bisimulations and other bisimulations for open processes is proved. Furthermore, we present a symbolic operational semantics of higher order open processes, and give some symbolic bisimulations for higher order processes. The relation between symbolic bisimulations and other bisimulations is also studied. At last, we introduce a higher order π-calculus with sum and conditional operators, then we study open bisimulations and symbolic bisimulations for this calculus.

Process algebra are a set of formal languages that are suitable to describe concurrent and communication systems including Web services. Nowadays, although process algebra have been effectively exploited for modeling and verifying functional aspects of Web services composition, non-functional aspects have been ignored due to process algebra lack of capability of modeling them. Since execution of Web services need to consume resource (and energy, time, fee, etc), we propose an abstract concept, that is, cost, to model this non-functional aspect. We introduce this abstract concept into TCCS(temporal calculus of communicating systems) that is a classical process algebra and propose a new process algebra called PTCCS(priced temporal calculus of communicating systems). We present syntax and semantics of PTCCS, and prove that PTCCS extends TCCS with cost modeling capability. And an algorithm is proposed to construct cost state space that is used to select Web services composition with optimal cost. Experiment results show that PTCCS can model both functional aspects and non-functional aspects of Web services composition.