In the course of understanding biological regulatory networks (BRN), scientists usually start by studying small BRNs that they believe to be of particular importance to represent a biological function, and then, embed...
详细信息
ISBN:
(纸本)9783540851004
In the course of understanding biological regulatory networks (BRN), scientists usually start by studying small BRNs that they believe to be of particular importance to represent a biological function, and then, embed them in the whole network. Such a reduction can lead to neglect relevant regulations and to study a network whose properties can be very different from the properties of this network viewed as a part of the whole. In this paper we study, from a logical point of view, the preservation of properties inherited from small BRNs. The signature of BRN, constituted by a graph, is one of the distinctive features on which embeddings can be defined which leads us to give a first condition on the subgraphs ensuring the preservation of properties of the embedded graphs.
This study focuses on automatic searching and verifying methods for the teachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic sear...
详细信息
This study focuses on automatic searching and verifying methods for the teachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic （CTL）. This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.
Validation is an important task in complex embedded system designs. A method of modelling and analysing embedded systems with programmable logic controllers is presented. Controllers and physical plants are modelled u...
详细信息
Validation is an important task in complex embedded system designs. A method of modelling and analysing embedded systems with programmable logic controllers is presented. Controllers and physical plants are modelled using timed automata. The system requirements are specified and formalised as computational tree logic properties. It is demonstrated that the designed model satisfies the required properties by resorting to a symbolic model checker, Uppaal, for real-time systems. A realistic example, the steeve controller of a theatre, illustrates the strategies. The safety and time constraint requirements are validated by Uppaal. The experimental results demonstrate the effectiveness of the approach presented here.
The Generalized Railway Crossing problem was defined as a benchmark problem for comparing different formal methods and methodologies developed for specifying and analysing mixed hardware/software systems. Various solu...
详细信息
ISBN:
(纸本)9788392263241
The Generalized Railway Crossing problem was defined as a benchmark problem for comparing different formal methods and methodologies developed for specifying and analysing mixed hardware/software systems. Various solutions of this problem were developed by the real-time researchers. The authors of this paper presents the model of a crossing controller specified in terms of coloured Petri nets. Important technical requirements of the controller are defined by means of temporal logics formulas. The problem had to be slightly redefined to omit the usage of time in the Petri net based model. Safety and Liveness properties were verified during the design process. Such an attempt should shorten the design phase and could be a very efficient tool for co-verification of the integrated design methodology.
This paper introduces a temporal epistemic logic CBCTL that updates agent's belief states through communications in them, based on computational tree logic (CTL). In practical environments, communication channels ...
详细信息
ISBN:
(纸本)9759845849
This paper introduces a temporal epistemic logic CBCTL that updates agent's belief states through communications in them, based on computational tree logic (CTL). In practical environments, communication channels between agents may not be secure, and in bad cases agents might suffer blackouts. In this study, we provide inform* protocol based on ACL of FIPA, and declare the presence of secure channels between two agents, dependent on time. Thus, the belief state of each agent is updated along with the progress of time. We show a prover, that is a reasoning system for a given formula in a given a situation of an agent;if it is directly provable or if it could be validated through the chains of communications, the system returns the proof.
This paper formalizes an incremental approach to design flow-control oriented hardware devices described by Moore machines. The method is based on successive additions of new behaviors to a simple device in order to b...
详细信息
This paper formalizes an incremental approach to design flow-control oriented hardware devices described by Moore machines. The method is based on successive additions of new behaviors to a simple device in order to build a more complex one. The new behaviors added must not override the previous ones. A set of CTL formulae is assigned to each step of the design. The links between the formulae of two consecutive design steps are formalized as a set of formula-transformations F, stating that : a CTL formula f is satisfied on a design at step i, iff F(f) is satisfied on the design extended at step i+1. This result has been applied during the design of bus protocol converters in the context on non-regression analysis. It could also be applied in order to simplify both system and formulae in particular cases.
Very often timing verification involves the analysis of the timings of discrete events such as signal changes, sending and receiving of signals, and sensitization of edge-triggered circuit components. The main bottlen...
详细信息
Very often timing verification involves the analysis of the timings of discrete events such as signal changes, sending and receiving of signals, and sensitization of edge-triggered circuit components. The main bottleneck in verifying timing properties of timed finite state machines (FSM) has been the inherent complexity of verifying timed properties (PSPACE-complete for timed extensions of computational tree logic (CTL)). Often however, we are interested in the best case or worst case timings between events. In this paper we introduce a temporal query language called Min-max Event-Triggered computational tree logic for expressing such extremal queries on the timings of events and show that such queries can be evaluated in time polynomial in the size of the system times the length of the formula.
暂无评论