A Hybrid Linear Logic for Constrained Transition Systems

Joelle Despeyroux 1 Kaustuv Chaudhuri 2
1 AxIS - Usage-centered design, analysis and improvement of information systems
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
Keywords : adequacy focusing stochastic pi-calculus hybrid logic linear logic
Type de document :
Communication dans un congrès
LIPIcs. TYPES 2013 - 19th International Conference on Types for Proofs and Programs, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014
Liste complète des métadonnées
https://hal.inria.fr/hal-01285039
Contributeur : Joelle Despeyroux <>
Soumis le : mardi 8 mars 2016 - 14:40:25
Dernière modification le : samedi 23 juin 2018 - 01:21:41
Document(s) archivé(s) le : dimanche 13 novembre 2016 - 10:37:51

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01285039, version 1
  • ARXIV : 1603.02641

Collections

X | LIX | INRIA | X-LIX | PARISTECH | X-DEP-INFO

Citation

Joelle Despeyroux, Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. LIPIcs. TYPES 2013 - 19th International Conference on Types for Proofs and Programs, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014. 〈hal-01285039〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

184

Téléchargements de fichiers

38

Contact


archive-ouverte@inria.fr