Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a (...) system, is explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence. (shrink)

This paper traces a relatively linear sequence of early research approaches to the formal verification of concurrent programs. It does so forwards and then backwards in time. After briefly outlining the context, the key insights from three distinct approaches from the 1970s are identified (Ashcroft/Manna, Ashcroft (solo) and Owicki). The main technical material in the paper focuses on a specific program taken from the last published of the three pieces of research (Susan Owicki’s): her own verification of her (...) _Findpos_ example is outlined followed by attempts at verifying the same example using the earlier approaches. Reconsidering the prior approaches on the basis of Owicki’s useful example illuminates similarities and differences between the proposals. Along the way, observations about interactions between researchers (and some “blind spots”) are noted. (shrink)

Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P (...) and A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. (shrink)

This unique volume introduces and discusses the methods of validating computer simulations in scientific research. The core concepts, strategies, and techniques of validation are explained by an international team of pre-eminent authorities, drawing on expertise from various fields ranging from engineering and the physical sciences to the social sciences and history. The work also offers new and original philosophical perspectives on the validation of simulations. Topics and features: introduces the fundamental concepts and principles related to the validation of computer simulations, (...) and examines philosophical frameworks for thinking about validation; provides an overview of the various strategies and techniques available for validating simulations, as well as the preparatory steps that have to be taken prior to validation; describes commonly used reference points and mathematical frameworks applicable to simulation validation; reviews the legal prescriptions, and the administrative and procedural activities related to simulation validation; presents examples of best practice that demonstrate how methods of validation are applied in various disciplines and with different types of simulation models; covers important practical challenges faced by simulation scientists when applying validation methods and techniques; offers a selection of general philosophical reflections that explore the significance of validation from a broader perspective. This truly interdisciplinary handbook will appeal to a broad audience, from professional scientists spanning all natural and social sciences, to young scholars new to research with computer simulations. Philosophers of science, and methodologists seeking to increase their understanding of simulation validation, will also find much to benefit from in the text. (shrink)

A thought experiment is reviewed which shows two things. First, in a region of a rotating frame that is not simply connected, the inertial forces can be canceled without completely canceling the inertial vector potential (whose curl determines the Coriolis force); second, the presence of this uncanceled potential can be detected in a quantum interference experiment. It is then argued that the thought experiment was realized in an earlier experiment involving a rotating superconductor, and that the experimental results confirm the (...) theoretical prediction. In this way, the first experimental verification of a physical effect due to a nonelectromagnetic potential in a force-free region is established. An analogous experiment for the gravitational vector potential is also discussed. Finally, it is pointed out that the close connection between electromagnetic and inertial vector potentials provides an intuitive way to make predictions about rotating superconductors. (shrink)

(1) It remains to be seen if in the field of Psychiatry just as in that of Psychology the verbal output of a subject can be submitted to verification. Many statements of a highly emotional character being merely symptoms of certain dispositions have no direct communicative sense at all.(2) It being one of the characteristics of the mentally ill to loose contact and exchange of ideas with other people, the question naturally suggests itself if this symptom may be at (...) the bottom of the phenomenon of these persons taking refuge in logical and ideological terminologies, their talk being a kind of verbal autism. (shrink)

(1) In contradistinction to mathematics, physics and biology, psychology and psychiatry deal to a large extent with the verbal behaviour of their objects. They are faced with two kinds of sense-problems: those with which the observer has to do in his theory-construction, and those which are characteristic of the verbal behaviour of his subjects.(2) Apart from a schematic and simplified usage, as it occurs in filling-up exercises and other laboratory verbal behaviour, the psychologist has to do with statements the sense (...) of which, on the one hand, is determined by the usage of his subjects and, on the other hand, so far as his records and theory are concerned, by his own language-sense. (shrink)

The paper is a part of the panel discussion with John Greco about his theory of the transmission of religious knowledge. My goal here is not to argue with Greco's theory, but to find out whether it requires any adjustment. I argue that Greco's theory of the social transmission of knowledge requires the transmitted knowledge to be socially verifiable, that is, to be subject to those means of confirmation that pertain to the social system. Unfortunately, some kinds of religious knowledge (...) are not socially verifiable; therefore, they cannot be transmitted via Greco's social mechanism. I conclude that Greco's theory turns out to be applicable to the socially verifiable religious testimonies, and not applicable to the rest. (shrink)

We investigate agents that have incomplete information and make decisions based on their beliefs expressed as situation calculus bounded action theories. Such theories have an infinite object domain, but the number of objects that belong to fluents at each time point is bounded by a given constant. Recently, it has been shown that verifying temporal properties over such theories is decidable. We take a first-person view and use the theory to capture what the agent believes about the domain of interest (...) and the actions affecting it. In this paper, we study verification of temporal properties over online executions. These are executions resulting from agents performing only actions that are feasible according to their beliefs. To do so, we first examine progression, which captures belief state update resulting from actions in the situation calculus. We show that, for bounded action theories, progression, and hence belief states, can always be represented as a bounded first-order logic theory. Then, based on this result, we prove decidability of temporal verification over online executions for bounded action theories. (shrink)

Ethics traditionally has always been derived from metaphysics, but these days metaphysics is considered to be "mere interpretation". In the face of all scepticism and relativism I contend that ethics is more certian than metaphysics. And so, ethics can ground metaphysics. And I go on, in later works to ground ethics on the Earth. Ethics has always had something to do with God. I redefine ethics, and open into God in a completely new way. That ethics brings us into relationship (...) with the living God and I have walked this path of relationship with Spirit for all of my life, and all of my works spring from it. (shrink)

Model checking techniques for communication protocols usually are phrased in terms of processes, basically labelled arcs in a labelled transition system. We propose to lift checking for such protocols to a more abstract level by analysing the protocols as composite communicative actions, with a communicative action viewed as a mapping on an appropriate class of epistemic models. As an example, we analyse an anonymous broadcast protocol (Chaum’s well-known dining cryptographers protocol) and an electronic voting protocol.

We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and rewrite CAPSL goals as temporal-epistemic specifications. We present a compiler that implements this translation. The compiler links to the symbolic model checker MCMAS. We evaluate the technique on protocols in the Clark-Jacobs library and in the SPORE repository against custom secrecy and authentication requirements.

The paper presents a novel method for the verification of security protocols’ time properties. The new method uses a translation to satisfiability modulo theories problem. In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and a BMC (...) algorithm. We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach. (shrink)

Mathematical statements arising from program verification are believed to be much easier to deal with than statements coming from serious mathematics. At least this is true for “normal programming”.

Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic (...) setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity. (shrink)

This study developed an online career adaptability improvement program as part of the undergraduate curriculum to improve college students’ career adaptability and verify its effectiveness. This 13-week intervention program, developed using the Korea-Career Adaptability Scale, consists of three domains: knowledge and recognition of the self and work environment, self-directed coping related to career behavior, and environmental interaction for career decisions and adaptation. Two sub-studies were conducted to achieve the research objectives: Study 1 included developing and testing a pilot program and (...) Study 2 quantitatively analyzed the final program to test its effectiveness. In Study 1, preliminary program development and validity were verified, and in Study 2, the effectiveness of the final program was verified. As a strategy to achieve the research purpose, in Study 1, literature review and needs analysis, program design reflecting the results of the needs analysis, validity verification through Delphi survey, preliminary program implementation and evaluation, and the operation of the final program were performed. To test the effectiveness of the program in Study 2, a pre-posttest of career adaptability was conducted on experimental, comparison, and control groups using the non-equivalent group pretest–posttest design, followed by a program satisfaction survey. This study is meaningful in that it developed an online program to help college students improve career adaptability and identified its effectiveness. This study yielded two results. First, it successfully developed a career adaptability improvement program for undergraduate students, wherein the career development tasks, and the sub-factors of career adaptability were organically interlinked. Second, it verified the statistically significant differences in the career adaptability scores among the experimental, comparison, and control groups. The highest mean score was obtained by participants in the experimental group, followed by the comparison and the control group. (shrink)

This paper studies the complexity of behavior of multi-agent systems. Behavior properties are formulated using classical temporal logic languages and are checked with respect to the transition system induced by the definition of the multi-agent system. We establish various tight complexity bounds of the behavior properties under natural structural and semantic restrictions on agent programs and actions.

We analyze the Michelson type experiment performed by Brillet and Hall. The order of magnitude of the gravitational effect (a beating frequency between two lasers) is calculated. We prove that Newtonian tidal forces could be observed when they originate from the oblateness of the Earth, from its rotation, from local masses, from the Moon or the Sun but not from the Galaxy (contrary to what has been recently claimed). We conclude that it is important to build a new parametrized theoretical (...) framework for the analysis of high-precision experiments. (shrink)