共查询到20条相似文献,搜索用时 31 毫秒
1.
O-Minimal Hybrid Systems 总被引:1,自引:0,他引:1
Gerardo Lafferriere George J. Pappas Shankar Sastry 《Mathematics of Control, Signals, and Systems (MCSS)》2000,13(1):1-21
An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of
a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original
infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal
hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous
dynamics for which finite bisimulations exist.
Date received: June 9, 1998. Date revised: June 28, 1999. 相似文献
2.
Automatic verification for a class of distributed systems 总被引:1,自引:0,他引:1
Summary. The paper presents a new analysis method for a class of concurrent systems which are formed of several interacting components
with the same structure. The model for these systems is composed of a control process and a set of homogeneous user processes. The control and user processes are modeled by finite labeled state transition systems which interact by means
of enabling functions and triggering mechanisms. Based on this structure, an analysis method is presented which allows system
properties, derived by reachability analysis for a finite number of user processes, to be generalized to an arbitrary number of user processes. A procedure for the automatic verification of properties such as mutual exclusion and absence of
deadlocks is presented and is then used to provide for the first time a fully automated verification of the Lamport's fast
mutual exclusion algorithm.
Received: October 1998/Accepted January 2000 相似文献
3.
Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We introduce a new general approach to regular model checking based on inference of regular languages. The method builds upon the observation that for infinite-state systems whose behaviour can be modelled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations up to a certain length n. These configurations are a (positive) sample of the reachable configurations of the given system, whereas all other words up to length n are a negative sample. Then, methods of inference of regular languages can be used to generalize the sample to the full reachability set (or an overapproximation of it). We have implemented our method in a prototype tool which shows that our approach is competitive on a number of concrete examples. Furthermore, in contrast to all other existing regular model checking methods, termination is guaranteed in general for all systems with regular sets of reachable configurations. The method can be applied in a similar way to dealing with reachability relations instead of reachability sets too. 相似文献
4.
We show how the tree-automata techniques proposed by Lugiez and Schnoebelen apply to the reachability analysis of RPPS systems. Using these techniques requires that we express the states of RPPS systems in a tailor-made process rewrite system where reachability is a relation recognizable by finite tree-automata. 相似文献
5.
Petri网的符号ZBDD可达树分析技术 总被引:2,自引:0,他引:2
Petri网是一种适合于并发系统建模、分析和控制的图形工具.可达树是Petri网分析的典型技术之一,它通过标识向量集合表征系统的状态空间,组合复杂性严重制约了该分析技术可处理系统问题的规模.零压缩决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)是一种新型的数据结构,是表示和处理稀疏向量集合的一种有效技术.文章基于Petri网町达标识向量的稀疏特征,给出了Petri网分析的符号ZBDD技术,该技术通过对标识向量(状态)的布尔向量表示、可达标识向最(状态)的符号ZBDD生成,实现Petri网可达状态空间的高效符号操作和紧凑符号表示.实验表明,基于ZBDD的符号可达性分析算法能够有效处理较大规模Petri网问题. 相似文献
6.
Notomi M. Murata T. 《IEEE transactions on pattern analysis and machine intelligence》1994,20(5):325-336
Petri nets have been proposed as a promising tool for modeling and analyzing concurrent-software systems such as Ada programs and communication protocol software. Among analysis techniques available for Petri nets, the most general approach is to generate all possible states (markings) of the system in a form of a so-called reachability graph. However, this conventional reachability graph approach is inefficient or intractable, even for a bounded Petri net, due to state explosion in many practical applications. To cope with this problem, this paper proposes a method for constructing a hierarchically organized state space called the hierarchical reachability graph (HRG). Using the HRG, we obtain necessary and sufficient conditions for reachability and deadlock, as well as algorithms to test whether a given state or marking is reachable from the initial state and whether there is a deadlock state (a state with no successor states) 相似文献
7.
SAT-Solving the Coverability Problem for Petri Nets 总被引:2,自引:0,他引:2
Parosh Aziz Abdulla S. Purushothaman Iyer Aletta Nylén 《Formal Methods in System Design》2004,24(1):25-43
Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993) showed that deadlock detection on unfoldings of 1-safe Petri nets is NP-complete. Since the deadlock problem on Petri nets is PSPACE-hard it is generally accepted that the two step process will yield savings (in time and space) provided the unfoldings are small.In this paper we show how unfoldings can be extended to the context of infinite-state systems. More precisely, we show how unfoldings can be constructed to represent sets of backward reachable states of unbounded Petri nets in a symbolic fashion. Furthermore, based on unfoldings, we show how to solve the coverability problem for unbounded Petri nets using a SAT-solver. Our experiments show that the use of unfoldings, in spite of the two-step process for solving coverability, has better time and space characteristics compared to a traditional reachability based implementation that considers all interleavings for solving the coverability problem. 相似文献
8.
Lei Bu Xuandong Li 《International Journal on Software Tools for Technology Transfer (STTT)》2011,13(4):307-317
The existing techniques for reachability analysis of linear hybrid systems do not scale well to the problem size of practical
interest. The performance of existing techniques is even worse for reachability analysis of a composition of several linear
hybrid automata. In this paper, we present an efficient path-oriented approach to bounded reachability analysis of composed
systems modeled by linear hybrid automata with synchronization events. It is suitable for analyzing systems with many components
by selecting critical paths, while this task was quite insurmountable before because of the state explosion problem. This
group of paths will be transformed to a group of linear constraints, which can be solved by a linear programming solver efficiently.
This approach of symbolic execution of paths allows design engineers to check important paths, and accordingly increase the
faith in the correctness of the system. This approach is implemented into a prototype tool Bounded reAchability CHecker (BACH).
The experimental data show that both the path length and the number of participant automata in a system checked using BACH
can scale up greatly to satisfy practical requirements. 相似文献
9.
Christopher L. Barrett Harry B. Hunt III Madhav V. Marathe S.S. Ravi Daniel J. Rosenkrantz Richard E. Stearns 《Journal of Computer and System Sciences》2006,72(8):1317-1345
Sequential Dynamical Systems (SDSs) are a special type of finite discrete dynamical systems that can be used to model simulation systems. We focus on the computational complexity of testing several phase space properties of SDSs. Our main result is a sharp delineation between classes of SDSs whose behavior is easy to predict and those whose behavior is hard to predict. Specifically, we show the following.
- 1.
- Several state reachability problems for SDSs are PSPACE-complete, even when restricted to SDSs whose underlying graphs are of bounded bandwidth (and hence of bounded pathwidth and treewidth), and the function associated with each node is symmetric. Moreover, this result holds even when the underlying graph is d-regular for some constant d and all the nodes compute the same symmetric Boolean function. An immediate corollary of this result is a PSPACE-hard lower bound on the complexity of reachability problems for regular generalized 1D-Cellular Automata and undirected systolic networks with Boolean totalistic local transition functions.
- 2.
- In contrast, the above reachability problems are solvable in polynomial time for SDSs when the Boolean function associated with each node is symmetric and monotone.
10.
Formal Description and Verification of a Transport Protocol for Local Networks 总被引:3,自引:0,他引:3 下载免费PDF全文
李腊元 《计算机科学技术学报》1990,5(1):64-70
11.
Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and that can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effective. We illustrate our exact acceleration technique with run-time data obtained with the model checkers Uppaal and Kronos. Moreover, we demonstrate that automated application of our exact acceleration technique can significantly speed-up the verification of the run-time behavior of LEGO Mindstorms programs. 相似文献
12.
Reachability analysis of real-time systems using time Petri nets 总被引:13,自引:0,他引:13
Wang J. Deng Y. Xu G. 《IEEE transactions on systems, man, and cybernetics. Part B, Cybernetics》2000,30(5):725-736
Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique for reachability analysis of TPNs, however, is not suitable for timing property verification because one cannot derive end-to-end delay in task execution, an important issue for time-critical systems, from the reachability tree constructed using the technique. In this paper, we present a new reachability based analysis technique for TPNs for timing property analysis and verification that effectively addresses the problem. Our technique is based on a concept called clock-stamped state class (CS-class). With the reachability tree generated based on CS-classes, we can directly compute the end-to-end time delay in task execution. Moreover, a CS-class can be uniquely mapped to a traditional state class based on which the conventional reachability tree is constructed. Therefore, our CS-class-based analysis technique is more general than the existing technique. We show how to apply this technique to timing property verification of the TPN model of a command and control (C2) system. 相似文献
13.
Rajeev Alur Costas Courcoubetis Thomas A. Henzinger 《Formal Methods in System Design》1997,11(2):137-155
We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem. 相似文献
14.
Verifying Programs with Unreliable Channels 总被引:1,自引:0,他引:1
We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels. 相似文献
15.
A term rewriting system is called growing if each variable occurring on both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-nonlinear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for right-ground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems. 相似文献
16.
This poses and solves the problem of structurally variable control synthesis for time-varying Lurie systems, which has both theoretical and engineering significance. A theorem on absolute stability of a set related to Lurie systems solves the problem. The theorem is basic for proving control algorithms that ensure absolute stability of a sliding subspace or its stability with finite reachability time. Moreover, they ensure the attraction in the whole of the zero equilibrium state of the whole control system of the plant on N(L). The selection of the sliding subspace can be such that the system nonlinearity does not influence the sliding motion. 相似文献
17.
18.
Thereachability, deadlok detection andunboundedness detection problems are considered for the class ofcyclic one-type message networks of communicating finite state machines. We show that all the three problems are effectively solvable by (a) constructing canonical execution event sequences which belong to a context-free language, and (b) showing that the reachability sets are semilinear. Our algorithms have polynomial complexity in terms of size of a global structure of a network, called theshuffle-product. The relationships between general Petri nets and the class of communicating finite state machines considered here are also explored.Supported in part by NSF CCR-9004121 相似文献
19.
O. Bournez 《Theory of Computing Systems》1999,32(1):35-67
We study the computational power of Piecewise Constant Derivative (PCD) systems. PCD systems are dynamical systems defined
by a piecewise constant differential equation and can be considered as computational machines working on a continuous space
with a continuous time. We show that the computation time of these machines can be measured either as a discrete value, called
discrete time, or as a continuous value, called continuous time. We relate the two notions of time for general PCD systems.
We prove that general PCD systems are equivalent to Turing machines and linear machines in finite discrete time. We prove
that the languages recognized by purely rational PCD systems in dimension d in finite continuous time are precisely the languages of the (d-2) th level of the arithmetical hierarchy. Hence the reachability problem of purely rational PCD systems of dimension d in finite continuous time is Σ
d-2
-complete.
Received May 1997, and in final form May 1998. 相似文献