To enhance the ability of current modeling system, an uniformed representation is designed to represent wire frame, solid, surface models. We present an algorithm for Boolean operation between the models under this r...To enhance the ability of current modeling system, an uniformed representation is designed to represent wire frame, solid, surface models. We present an algorithm for Boolean operation between the models under this representation. Accuracy, efficiency and robustness are the main consideration. The geometric information is represented with trimmed parametric patches and trimmed parametric splines. The topological information is represented with an extended half edge data structure. In the process of intersection calculation, hierarchy intersection method is applied for unified classification. Tracing the intersection curve to overcome degenerate cases that occur frequently in practice. The algorithm has been implemented as the modeling kernel of a feature based modeling system named GS CAD98, which was developed on Windows/NT platform.展开更多
Boolean control network consists of a set of Boolean variables whose state is determined by other variables in the network. Boolean network is used for modeling complex system. In this paper, we have presented a model...Boolean control network consists of a set of Boolean variables whose state is determined by other variables in the network. Boolean network is used for modeling complex system. In this paper, we have presented a model of a context-aware system used in smart home based on Boolean control networks. This modeling describes the relationship between the context elements (person, time, location, and activity) and services (Morning Call, Sleeping, Guarding, Entertainment, and normal), which is effective to logical inference. We apply semi tensor matrix product to describe the dynamic of the system. This matrix form of expression is a convenient and reasonable way to design logic control system.展开更多
In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the...In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.展开更多
A polyhedral solid modeler that operates on boundary representations (B-reps) of ob- jects must derive topological information from numerical data.Due to finite precision of the com- puter,unavoidable numerical calcul...A polyhedral solid modeler that operates on boundary representations (B-reps) of ob- jects must derive topological information from numerical data.Due to finite precision of the com- puter,unavoidable numerical calculation errors may result in ambiguous or contradictory decision of topology.These effects cause existing polyhedral modelers to fail when confronted with objects that nearly align or barely intersect. Based on analysing the reasons which cause the failure of Boolean operation to fail,this paper describes an algorithm using solid integrity to carefully design each step of Boolean operation,so that valid polyhedral modeling results may be achieved.展开更多
As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the ...As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.展开更多
Background:A novel data-driven Boolean model,namely,the fundamental Boolean model(FBM),has been proposed to draw genetic regulatory insights into gene activation,inhibition,and protein decay,published in 2018.This nov...Background:A novel data-driven Boolean model,namely,the fundamental Boolean model(FBM),has been proposed to draw genetic regulatory insights into gene activation,inhibition,and protein decay,published in 2018.This novel Boolean model facilitates the analysis of the activation and inhibition pathways.However,the novel model does not handle the situation well,where genetic regulation might require more time steps to complete.Methods:Here,we propose extending the fundamental Boolean modelling to address the issue that some gene regulations might require more time steps to complete than others.We denoted this extension model as the temporal fundamental Boolean model(TFBM)and related networks as the temporal fundamental Boolean networks(TFBNs).The leukaemia microarray datasets downloaded from the National Centre for Biotechnology Information have been adopted to demonstrate the utility of the proposed TFBM and TFBNs.Results:We developed the TFBNs that contain 285 components and 2775 Boolean rules based on TFBM on the leukaemia microarray datasets,which are in the form of short-time series.The data contain gene expression measurements for 13 GC-sensitive children under therapy for acute lymphoblastic leukaemia,and each sample has three time points:0 hour(before GC treatment),6/8 hours(after GC treatment)and 24 hours(after GC treatment).Conclusion:We conclude that the proposed TFBM unlocks their predecessor’s limitation,Le.,FBM,that could help pharmaceutical agents identify any side effects on clinic-related data.New hypotheses could be identified by analysing the extracted fundamental Boolean networks and analysing their up-regulatory and down-regulatory pathways.展开更多
文摘To enhance the ability of current modeling system, an uniformed representation is designed to represent wire frame, solid, surface models. We present an algorithm for Boolean operation between the models under this representation. Accuracy, efficiency and robustness are the main consideration. The geometric information is represented with trimmed parametric patches and trimmed parametric splines. The topological information is represented with an extended half edge data structure. In the process of intersection calculation, hierarchy intersection method is applied for unified classification. Tracing the intersection curve to overcome degenerate cases that occur frequently in practice. The algorithm has been implemented as the modeling kernel of a feature based modeling system named GS CAD98, which was developed on Windows/NT platform.
文摘Boolean control network consists of a set of Boolean variables whose state is determined by other variables in the network. Boolean network is used for modeling complex system. In this paper, we have presented a model of a context-aware system used in smart home based on Boolean control networks. This modeling describes the relationship between the context elements (person, time, location, and activity) and services (Morning Call, Sleeping, Guarding, Entertainment, and normal), which is effective to logical inference. We apply semi tensor matrix product to describe the dynamic of the system. This matrix form of expression is a convenient and reasonable way to design logic control system.
文摘In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.
文摘A polyhedral solid modeler that operates on boundary representations (B-reps) of ob- jects must derive topological information from numerical data.Due to finite precision of the com- puter,unavoidable numerical calculation errors may result in ambiguous or contradictory decision of topology.These effects cause existing polyhedral modelers to fail when confronted with objects that nearly align or barely intersect. Based on analysing the reasons which cause the failure of Boolean operation to fail,this paper describes an algorithm using solid integrity to carefully design each step of Boolean operation,so that valid polyhedral modeling results may be achieved.
基金Supported by the National Natural Science Foundation of China(Nos.61063002,61100186,61262008)Guangxi Natural Science Foundation of China(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220)the Key Project of Education Department of Guangxi
文摘As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.
文摘Background:A novel data-driven Boolean model,namely,the fundamental Boolean model(FBM),has been proposed to draw genetic regulatory insights into gene activation,inhibition,and protein decay,published in 2018.This novel Boolean model facilitates the analysis of the activation and inhibition pathways.However,the novel model does not handle the situation well,where genetic regulation might require more time steps to complete.Methods:Here,we propose extending the fundamental Boolean modelling to address the issue that some gene regulations might require more time steps to complete than others.We denoted this extension model as the temporal fundamental Boolean model(TFBM)and related networks as the temporal fundamental Boolean networks(TFBNs).The leukaemia microarray datasets downloaded from the National Centre for Biotechnology Information have been adopted to demonstrate the utility of the proposed TFBM and TFBNs.Results:We developed the TFBNs that contain 285 components and 2775 Boolean rules based on TFBM on the leukaemia microarray datasets,which are in the form of short-time series.The data contain gene expression measurements for 13 GC-sensitive children under therapy for acute lymphoblastic leukaemia,and each sample has three time points:0 hour(before GC treatment),6/8 hours(after GC treatment)and 24 hours(after GC treatment).Conclusion:We conclude that the proposed TFBM unlocks their predecessor’s limitation,Le.,FBM,that could help pharmaceutical agents identify any side effects on clinic-related data.New hypotheses could be identified by analysing the extracted fundamental Boolean networks and analysing their up-regulatory and down-regulatory pathways.
