We investigate the decidability of model checking logics of time, knowledge, and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observable discret...
详细信息
We investigate the decidability of model checking logics of time, knowledge, and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observable discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular, for the synchronous perfect recall semantics, a generalization from temporal operators with finite reach to operators with infinite reach renders model checking undecidable. The case of the clock semantics is closely related to a monadic second-order logic of time and probability that is known to be decidable, except on a set of measure zero. We show that two distinct extensions of this logic make model checking undecidable. One of these involves polynomial combinations of probability terms, the other involves monadic second-order quantification into the scope of probability operators. These results explain some of the restrictions in previous work.
logics of knowledge and knowledge-based programs provide a way to give abstract descriptions of solutions to problems in fault-tolerant distributed computing, and have been used to derive optimal protocols for these p...
详细信息
ISBN:
(纸本)9798400718854
logics of knowledge and knowledge-based programs provide a way to give abstract descriptions of solutions to problems in fault-tolerant distributed computing, and have been used to derive optimal protocols for these problems with respect to a variety of failure models. Generally, these results have involved complex pencil and paper analyses with respect to the theoretical "full-information protocol" model of information exchange between network nodes. It is equally of interest to be able to establish the optimality of protocols using weaker, but more practical, models of information exchange, or else identify opportunities to improve their performance. Over the last 20 years, automated verification and synthesis tools for the logic of knowledge have been developed, such as the model checker MCK, that can be applied to this problem. This paper concerns the application of MCK to automated analyses of this kind. A number of information-exchange models are considered, for Simultaneous and Eventual variants of Byzantine Agreement under a range of failure types. MCK is used to automatically analyze these models. The results demonstrate that it is possible to automatically identify optimization opportunities, and to automatically synthesize optimal protocols. The paper provides performance measurements for the automated analysis, establishing a benchmark for epistemic model checking and synthesis tools.
The ability of reasoning about knowledge and strategy is key to the autonomy of an intelligent system of multiple players. In this paper, we study the logic of knowledge and strategy in stochastic multi-agent systems,...
详细信息
ISBN:
(纸本)9781450319935
The ability of reasoning about knowledge and strategy is key to the autonomy of an intelligent system of multiple players. In this paper, we study the logic of knowledge and strategy in stochastic multi-agent systems, where the system's behaviour is determined by both the behaviour of the players and by some random elements. Players have incomplete information about the system and do not have memory. A logic PATEL*, whose semantics is based on partially-observed concurrent game structures, is proposed. The computational complexities of model checking the logic and its sublogics are solved.
作者：
Herzig, AndreasIRIT
CNRS University of Toulouse IRIT Toulouse Cedex 9 France
Dynamic epistemic logics provide an account of the evolution of agents’ belief and knowledge when they learn the occurrence of an event. These logics started to become popular about 20 years ago and by now there exis...
详细信息
We overview the most prominent logics of knowledge and action that were proposed and studied in the multiagent systems literature. We classify them according to these two dimensions, knowledge and action, and moreover...
详细信息
We overview the most prominent logics of knowledge and action that were proposed and studied in the multiagent systems literature. We classify them according to these two dimensions, knowledge and action, and moreover introduce a distinction between individual knowledge and group knowledge, and between a nonstrategic an a strategic interpretation of action operators. For each of the logics in our classification we highlight problematic properties. They indicate weaknesses in the design of these logics and call into question their suitability to represent knowledge and reason about it. This leads to a list of research challenges.
Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an ...
详细信息
ISBN:
(纸本)9783642414886;9783642414879
Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an online auction system we may want to ensure that no bidder knows the bids of any other bidder before the auction is closed. Such systems are typically interactive/reactive and communication is mostly asynchronous, lossy or unordered. Language-based security provides language mechanisms for enforcing end-to-end security. However, with few exceptions, previous research has mainly focused on relational or synchronous models, which are generally not suitable for distributed systems. This paper proposes a general knowledge-based account of possibilistic security from a language perspective and shows how existing trace-based conditions fit in. A syntactic characterization of these conditions, given by an epistemic temporal logic, shows that existing model checking tools can be used to enforce security.
Diagnosability is a key attribute of systems to enable the detection of failure events by partial observations. This paper addresses the diagnosability in concurrent probabilistic systems. Four different notions (L-, ...
详细信息
ISBN:
(纸本)9781450319935
Diagnosability is a key attribute of systems to enable the detection of failure events by partial observations. This paper addresses the diagnosability in concurrent probabilistic systems. Four different notions (L-, P-, A-, and AA-diagnosability) are characterised by formulas of a logic of knowledge, time and probability. Also, we investigate the computational complexities of verifying them: the L-diagnosability is NL-complete, the A-diagnosability is PTIME-complete, and the P-diagnosability is in PSPACE.
The construction of the curriculum framework should not only comply with the general requirements of the curriculum development,but also take account of the specialty of different majors and different *** present,the ...
详细信息
The construction of the curriculum framework should not only comply with the general requirements of the curriculum development,but also take account of the specialty of different majors and different *** present,the study of the curriculum development of college education still leaves much to be desired,especially in Physical *** paper,based on the general principles and domestic and foreign research and combined with the problems in practice,discusses the train of thought and the method of working out the curriculum framework of the PE major,aiming at providing references for the reform of the curriculum.
This paper is written to draw attention to the ideal knower and the logic of knowledge embedded in curricula. New logics and new knowers, I argue, are conjured with the hope they will be capable of succeeding in curri...
详细信息
This paper is written to draw attention to the ideal knower and the logic of knowledge embedded in curricula. New logics and new knowers, I argue, are conjured with the hope they will be capable of succeeding in curriculum designers' imagined future. I frame this discussion in terms of debates about the place of knowledge in the sociology of education. knowledge and knowers are produced together in curriculum, and it is useful to keep them together in studying classrooms. The bulk of the paper is a detailed comparison of two curricula written for the Australian state of Victoria. I will show that one - the 2000 Curriculum Standards Framework, second edition - follows a logic of truth. The second - the 2007 Victorian Essential Learning Standards - follows a logic of realisation. These contrasting logics require and instantiate quite different types of knower.
Larry Moss and Rohit Parikh used subset semantics to characterize a family of logics for reasoning about knowledge. An important feature of their framework is that subsets always decrease based on the assumption that ...
详细信息
Larry Moss and Rohit Parikh used subset semantics to characterize a family of logics for reasoning about knowledge. An important feature of their framework is that subsets always decrease based on the assumption that knowledge always increases. We drop this assumption and modify the semantics to account for logics of knowledge that handle arbitrary changes, that is, changes that do not necessarily result in knowledge increase, such as the update of our knowledge due to an action. We present a system which is complete for subset spaces and prove its decidability.
暂无评论