scholarly journals Modeling and Verifying the CKB Blockchain Consensus Protocol

Mathematics ◽  
2021 ◽  
Vol 9 (22) ◽  
pp. 2954
Author(s):  
Meng Sun ◽  
Yuteng Lu ◽  
Yichun Feng ◽  
Qi Zhang ◽  
Shaoying Liu

The Nervos CKB (Common Knowledge Base) is a public permissionless blockchain designed for the Nervos ecosystem. The CKB consensus protocol is the key protocol of the Nervos CKB, which improves the limit of the consensus’s performance for Bitcoin. In this paper, we developed the formal model of the CKB consensus protocol using timed automata. Based on the model, we formally verified various important properties of the Nervos CKB to provide a sufficient trustworthiness assurance. Especially, the security of the Nervos CKB against the selfish mining attacks to the protocol was investigated.

Author(s):  
Fateh Latreche ◽  
Faiza Belala

Web services are very dynamic, they are all around us and we use them every day without even knowing it. In this paper, the authors define a formal model for dynamic Web services composition and they investigate how it can be used to specify and analyse backward recovery procedures, updating partner services in case of failure. First, they propose Recursive and Dynamic Timed Automata (RDTA) model, interpreted over composite service configurations, which provide a natural way to design stateful and dynamic Web services. Then, the authors define the concurrent semantics of this timed automata extension in terms of real-time rewrite theories. Analysis of the model is carried out in the Real-Time Maude system, based on checking relevant properties.


2020 ◽  
Vol 87 (S1) ◽  
pp. 122-127 ◽  
Author(s):  
Sabine Ferneborg ◽  
Fabio Napolitano ◽  
Mette Vaarst ◽  
Cecilie M. Mejdell ◽  
Susanne Waiblinger ◽  
...  

AbstractThis position paper describes a common stand on methodology of human attitudes and behaviour that is suitable to use in studies regarding cow−calf contact (CCC) in dairy production, in order to create a common knowledge base and foundation for future recommendations of CCC systems. We describe how different quantitative and qualitative methods can be used to study human attitudes to CCC as well as farmer or consumer behaviour. We aim to contribute to a better understanding of the available methods, and hope that this paper can be used as a guideline for future studies in this area.


2005 ◽  
Vol 2 (1) ◽  
pp. 1-29
Author(s):  
John Debenham

Knowledge base maintenance is managed by constructing a formal model. In this model the representation of each chunk of know ledge encapsulates the knowledge in a set of declarative rules, each of which in turn encapsulates the knowledge in a set of imperative programs. In this model an "item" is the unit of knowledge representation. Items are at a higher level of abstraction than rules. Understanding what has to be done to maintain the integrity of an item leads to a specification of the modifications to the set of programs that implement it. An analysis of the maintenance of the formal model is achieved by introducing maintenance links. Analysis of the maintenance links shows that they are of four different types. The density of the maintenance links is reduced by transforming that set into an equivalent set. In this way the knowledge base maintenance problem is analyzed and simplified. A side benefit of knowledge items as a formalism is that they contain knowledge constraints that protect the knowledge from unforeseen modification.


2009 ◽  
Vol 35 ◽  
pp. 677-716 ◽  
Author(s):  
K. Su ◽  
A. Sattar ◽  
G. Lv ◽  
Y. Zhang

In this paper, we investigate knowledge reasoning within a simple framework called knowledge structure. We use variable forgetting as a basic operation for one agent to reason about its own or other agents\' knowledge. In our framework, two notions namely agents\' observable variables and the weakest sufficient condition play important roles in knowledge reasoning. Given a background knowledge base and a set of observable variables for each agent, we show that the notion of an agent knowing a formula can be defined as a weakest sufficient condition of the formula under background knowledge base. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. Also, we show that public announcement operator can be conveniently dealt with via our notion of knowledge structure. Further, we explore the computational complexity of the problem whether an epistemic formula is realized in a knowledge structure. In the general case, this problem is PSPACE-hard; however, for some interesting subcases, it can be reduced to co-NP. Finally, we discuss possible applications of our framework in some interesting domains such as the automated analysis of the well-known muddy children puzzle and the verification of the revised Needham-Schroeder protocol. We believe that there are many scenarios where the natural presentation of the available information about knowledge is under the form of a knowledge structure. What makes it valuable compared with the corresponding multi-agent S5 Kripke structure is that it can be much more succinct.


2021 ◽  
Vol 5 (Supplement_1) ◽  
pp. 769-769
Author(s):  
Paris Strom

Abstract This presentation hypothesizes that an innovative collaboration by the adult generations will be necessary to enable conditions needed for family success in a longevity society. Unprecedented challenges of parents and grandparents are examined. Reasons why adults have to regard youth as a source of learning about their unique experiences in an age-separated society are explained. International curriculum development studies to support families of children from birth through adolescence are described. A curriculum that provides a common knowledge base about child and adolescent guidance is proposed to harmonize efforts of adults to support younger relatives. Curriculum for retirees should focus on continuing responsibilities other generations expect of them, learning about the lives of younger family members, and gaining awareness of parenting practices to reinforce lessons. Training volunteers in assisted living and long-term care facilities to be indigenous leaders of grandparent classes is discussed as a practical way to offer relevant learning and improve social support. Instruments are examined that assess ethnic relationships between adult generations, adults and adolescents, and track results of education intervention.


1979 ◽  
Vol 10 (3) ◽  
pp. 148-153
Author(s):  
Fred R. McFarlane ◽  
Suzanne M. Di Paola

After a comparative review of the roles and functions of the rehabilitation counselor, vocational evaluator, and work adjustment specialist the following discusses: (a) the duties and responsibilities; (b) the knowledges, skills and attitudes and; (c) the work settings peculiar to each of these three groups of professionals. Within its summary and recommendation, the paper suggests that (a) these three professionals should strive toward the same goal—client movement toward vocational independence; (b) these three groups bring a common knowledge base to the rehabilitative process; and (c) each individual professional has refined skills in each of the common knowledge areas. Specific recommendations for facilitating professional integration among these three groups are also included.


Sign in / Sign up

Export Citation Format

Share Document