scholarly journals A Substructural Modal Logic of Utility

2017 ◽  
Vol 27 (5) ◽  
pp. 1421-1464
Author(s):  
Gabrielle Anderson ◽  
David Pym
Keyword(s):  
Resource Allocation ◽  
Nash Equilibrium ◽  
Modal Logic ◽  
Process Algebra ◽  
Separation Logic ◽  
Cost Strategy ◽  
Soundness And Completeness ◽  
Concurrent Separation Logic ◽  
Resource Semantics ◽  
Best Responses

Abstract We introduce a substructural modal logic of utility that can be used to reason aboutoptimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy—Milner soundness and completeness hold. By considering notions of cost, strategy and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.

scholarly journals Cosmo: a concurrent separation logic for multicore OCaml

2020 ◽  
Vol 4 (ICFP) ◽  
pp. 1-29
Author(s):  
Glen Mével ◽  
Jacques-Henri Jourdan ◽  
François Pottier
Keyword(s):  
Separation Logic ◽  
Concurrent Separation Logic

Modal Logic and Equality for Process Algebra

1996 ◽  
Vol 6 (1) ◽  
pp. 121-136
Author(s):  
WILLIAM P. R. MITCHELL
Keyword(s):  
Modal Logic ◽  
Process Algebra

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

scholarly journals TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

2021 ◽  
Vol 43 (4) ◽  
pp. 1-134
Author(s):  
Emanuele D’Osualdo ◽  
Julian Sutherland ◽  
Azadeh Farzan ◽  
Philippa Gardner
Keyword(s):  
Case Studies ◽  
Separation Logic ◽  
Proof System ◽  
Concurrent Programs ◽  
Semantic Model ◽  
Compositional Reasoning ◽  
Fine Grained ◽  
Fundamental Innovation ◽  
Concurrent Separation Logic

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.

Classes of Potential Games

2017 ◽  
Author(s):  
João P. Hespanha
Keyword(s):  
Resource Allocation ◽  
Nash Equilibrium ◽  
Nash Equilibria ◽  
Potential Games ◽  
Congestion Games ◽  
Fictitious Play ◽  
Resource Allocation Problem ◽  
Distributed Resource Allocation ◽  
Symmetric Games ◽  
The Cost

This chapter discusses several classes of potential games that are common in the literature and how to derive the Nash equilibrium for such games. It first considers identical interests games and dummy games before turning to decoupled games and bilateral symmetric games. It then describes congestion games, in which all players are equal, in the sense that the cost associated with each resource only depends on the total number of players using that resource and not on which players use it. It also presents other potential games, including the Sudoku puzzle, and goes on to analyze the distributed resource allocation problem, the computation of Nash equilibria for potential games, and fictitious play. It concludes with practice exercises and their corresponding solutions, along with additional exercises.

scholarly journals EVERYONE KNOWS THAT SOMEONE KNOWS: QUANTIFIERS OVER EPISTEMIC AGENTS

2019 ◽  
Vol 12 (2) ◽  
pp. 255-270 ◽  
Author(s):  
PAVEL NAUMOV ◽  
JIA TAO
Keyword(s):  
Modal Logic ◽  
Epistemic Logic ◽  
Possible Worlds ◽  
Completeness Theorem ◽  
Kripke Semantics ◽  
Possible Worlds Semantics ◽  
Distributed Knowledge ◽  
First Order ◽  
Soundness And Completeness ◽  
First Order Modal Logic

AbstractModal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

Sign in / Sign up

Export Citation Format

Share Document