Logic in Computer Science

Authors and titles for April 2015

[26] arXiv:1504.04115 [pdf, other]

Title: FO Model Checking on Posets of Bounded Width

Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov, Jan Obdržálek, Sebastian Ordyniak, M. S. Ramanujan, Saket Saurabh

Comments: Minor correction, p.5, def. of τ_{s+1}: instead of an induced subdigraph of D_s, we use the appropriate relational structure formed from this subdigrph

Subjects: Logic in Computer Science (cs.LO); Discrete Mathematics (cs.DM)

[27] arXiv:1504.04152 [pdf, other]

Title: Interaction Graphs: Full Linear Logic

Thomas Seiller

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[28] arXiv:1504.04311 [pdf, other]

Title: Higher category models of the pi-calculus

Mike Stay, Lucius Gregory Meredith

Subjects: Logic in Computer Science (cs.LO)

[29] arXiv:1504.04662 [pdf, other]

Title: Permissive Controller Synthesis for Probabilistic Systems

Klaus Drager (Queen Mary, University of London), Vojtech Forejt (University of Oxford), Marta Kwiatkowska (University of Oxford), David Parker (University of Birmingham), Mateusz Ujma (University of Oxford)

Journal-ref: Logical Methods in Computer Science, Volume 11, Issue 2 (June 30, 2015) lmcs:1576

Subjects: Logic in Computer Science (cs.LO); Systems and Control (eess.SY); Optimization and Control (math.OC)

[30] arXiv:1504.04708 [pdf, other]

Title: The model checking fingerprints of CTL operators

Andreas Krebs, Arne Meier, Martin Mundhenk

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[31] arXiv:1504.04759 [pdf, other]

Title: On the Identity Type as the Type of Computational Paths

Arthur F. Ramos, Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira

Comments: 16 pages

Subjects: Logic in Computer Science (cs.LO)

[32] arXiv:1504.05038 [pdf, other]

Title: Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)

Ali Assaf

Comments: Long version of TLCA 2015 paper

Subjects: Logic in Computer Science (cs.LO)

[33] arXiv:1504.05739 [pdf, other]

Title: Faster Statistical Model Checking for Unbounded Temporal Properties

Przemysław Daca, Thomas A. Henzinger, Jan Křetínský, Tatjana Petrov

Comments: Published in the proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016

Subjects: Logic in Computer Science (cs.LO)

[34] arXiv:1504.05797 [pdf, other]

Title: Service-Oriented Logic Programming

Ionut Tutu (Department of Computer Science, Royal Holloway University of London), Jose Luiz Fiadeiro (Department of Computer Science, Royal Holloway University of London)

Journal-ref: Logical Methods in Computer Science, Volume 11, Issue 3 (August 18, 2015) lmcs:1579

Subjects: Logic in Computer Science (cs.LO)

[35] arXiv:1504.06105 [pdf, other]

Title: Model Checking Constraint LTL over Trees

Alexander Kartzow, Thomas Weidner

Subjects: Logic in Computer Science (cs.LO)

[36] arXiv:1504.06135 [pdf, other]

Title: Complexity of Propositional Logics in Team Semantics

Miika Hannula, Juha Kontinen, Jonni Virtema, Heribert Vollmer

Comments: 15 pages + 1 page appendix, the main result is generalised and the title updated to reflect this

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Logic (math.LO)

[37] arXiv:1504.06187 [pdf, other]

Title: LTL Fragments are Hard for Standard Parameterisations

Martin Lück, Arne Meier

Comments: TIME 2015 conference version

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[38] arXiv:1504.06203 [pdf, other]

Title: A New Thesis concerning Synchronised Parallel Computing - Simplified Parallel ASM Thesis

Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec, Qing Wang

Journal-ref: Theoretical Computer Science, 2016, Volume 649, 11 October 2016, Pages 25--53

Subjects: Logic in Computer Science (cs.LO)

[39] arXiv:1504.06355 [pdf, other]

Title: On Freeze LTL with Ordered Attributes

Normann Decker, Daniel Thoma

Comments: Extended version of article published in proceedings of FoSSaCS 2016

Subjects: Logic in Computer Science (cs.LO)

[40] arXiv:1504.06409 [pdf, other]

Title: Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics

Lauri Hella, Antti Kuusisto, Arne Meier, Heribert Vollmer

Comments: Correction of MFCS 2015 paper

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[41] arXiv:1504.06534 [pdf, other]

Title: An Automata-Theoretic Approach to the Verification of Distributed Algorithms

C. Aiswarya, Benedikt Bollig, Paul Gastin

Comments: 26 pages, 6 figures

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[42] arXiv:1504.06986 [pdf, other]

Title: Proof Theory of a Multi-Lane Spatial Logic

Sven Linker (Carl von Ossietzky Universität Oldenburg), Martin Hilscher (Carl von Ossietzky Universität Oldenburg)

Comments: This paper is the extended and slightly revised version of our publication in the 10th International Colloquium on Theoretical Aspects of Computing (ICTAC) in 2013

Journal-ref: Logical Methods in Computer Science, Volume 11, Issue 3 (August 18, 2015) lmcs:1580

Subjects: Logic in Computer Science (cs.LO)

[43] arXiv:1504.07003 [pdf, other]

Title: A Graph Theoretic Perspective on CPM(Rel)

Daniel Marsden (University of Oxford)

Comments: In Proceedings QPL 2015, arXiv:1511.01181

Journal-ref: EPTCS 195, 2015, pp. 273-284

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[44] arXiv:1504.07737 [pdf, other]

Title: A Simple Probabilistic Extension of Modal Mu-calculus

Wanwei Liu, Lei Song, Ji Wang, Lijun Zhang

Subjects: Logic in Computer Science (cs.LO)

[45] arXiv:1504.08309 [pdf, other]

Title: Refining Existential Properties in Separation Logic Analyses

Matko Botinčan, Mike Dodds, Stephen Magill

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[46] arXiv:1504.08321 [pdf, other]

Title: Evaluation trees for proposition algebra

Jan A. Bergstra, Alban Ponse

Comments: 34 pages, 1 table; main differences with v2: some proofs are corrected and/or simplified in S.3-6

Subjects: Logic in Computer Science (cs.LO)

[47] arXiv:1504.00134 (cross-list from math.FA) [pdf, other]

Title: From Haar to Lebesgue via Domain Theory, Revised version

Will Brian, Michael Mislove

Comments: This is a revised version of an earlier paper. The original claimed that all Haar measures on C are the same, which is not true. This version corrects that error

Subjects: Functional Analysis (math.FA); Logic in Computer Science (cs.LO); Group Theory (math.GR)

[48] arXiv:1504.01708 (cross-list from cs.GT) [pdf, other]

Title: Reactive Synthesis Without Regret

Paul Hunter, Guillermo A. Pérez, Jean-François Raskin

Comments: Fixed inaccuracies spotted by Udi Boker and Karoliina Lehtinen and improved the presentation of a few proofs

Subjects: Computer Science and Game Theory (cs.GT); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[49] arXiv:1504.01789 (cross-list from math.LO) [pdf, other]

Title: The Lattice of Congruences of a Finite Line Frame

Carlos Areces, Miguel Campercholi, Daniel Penazzi, Pedro Sánchez Terraf

Comments: 31 pages, 11 figures. Expanded intro, conclusions rewritten. New, less geometrical, proofs of Lemma 19 and (former) Lemma 34

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[50] arXiv:1504.02297 (cross-list from math.CT) [pdf, other]

Title: Formalizing parity complexes

Mitchell Buckley

Comments: Second version following revision for publication, 27 pages

Subjects: Category Theory (math.CT); Logic in Computer Science (cs.LO)

[51] arXiv:1504.02395 (cross-list from quant-ph) [pdf, other]

Title: Bridging the gap between general probabilistic theories and the device-independent framework for nonlocality and contextuality

Giulio Chiribella, Xiao Yuan

Comments: 61 pages, no figures, published version

Journal-ref: Information and Computation, 250, 15-49 (2016)

Subjects: Quantum Physics (quant-ph); Cryptography and Security (cs.CR); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO); Mathematical Physics (math-ph)

[52] arXiv:1504.02611 (cross-list from cs.SE) [pdf, other]

Title: Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model

Alexander Heußner, Christopher M. Poskitt, Claudio Corrodi, Benjamin Morandi

Comments: In Proceedings GaM 2015, arXiv:1504.02448

Journal-ref: EPTCS 181, 2015, pp. 32-47

Subjects: Software Engineering (cs.SE); Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[53] arXiv:1504.02612 (cross-list from cs.SI) [pdf, other]

Title: A Visual Analytics Approach to Compare Propagation Models in Social Networks

Jason Vallet (LaBRI, Univ. Bordeaux, France), Hélène Kirchner (Inria, Bordeaux, France), Bruno Pinaud (LaBRI, Univ. Bordeaux, France), Guy Melançon (LaBRI, Univ. Bordeaux, France)

Comments: In Proceedings GaM 2015, arXiv:1504.02448

Journal-ref: EPTCS 181, 2015, pp. 65-79

Subjects: Social and Information Networks (cs.SI); Logic in Computer Science (cs.LO)

[54] arXiv:1504.02614 (cross-list from cs.SE) [pdf, other]

Title: Improved Conflict Detection for Graph Transformation with Attributes

Géza Kulcsár (Technische Universität Darmstadt Real-Time Systems Lab), Frederik Deckwerth (Technische Universität Darmstadt Real-Time Systems Lab), Malte Lochau (Technische Universität Darmstadt Real-Time Systems Lab), Gergely Varró (Technische Universität Darmstadt Real-Time Systems Lab), Andy Schürr (Technische Universität Darmstadt Real-Time Systems Lab)

Comments: In Proceedings GaM 2015, arXiv:1504.02448

Journal-ref: EPTCS 181, 2015, pp. 97-112

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[55] arXiv:1504.02651 (cross-list from cs.FL) [pdf, other]

Title: Reachability analysis of first-order definable pushdown systems

Lorenzo Clemente, Sławomir Lasota

Comments: to appear in CSL'15

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[56] arXiv:1504.02730 (cross-list from math.OA) [pdf, other]

Title: Domains of commutative C*-subalgebras

Chris Heunen, Bert Lindenhovius

Comments: 42 pages

Journal-ref: Mathematical Structures in Computer Science, 29(7):972-1006, 2019

Subjects: Operator Algebras (math.OA); Logic in Computer Science (cs.LO)

[57] arXiv:1504.02796 (cross-list from cs.CR) [pdf, other]

Title: Model Counting Modulo Theories

Quoc-Sang Phan

Comments: PhD thesis (2015); Queen Mary University of London (this http URL)

Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)

[58] arXiv:1504.03014 (cross-list from cs.SE) [pdf, other]

Title: Proceedings 6th Workshop on Formal Methods and Analysis in SPL Engineering

Joanne M. Atlee (University of Waterloo, Canada), Stefania Gnesi (CNR-ISTI, Italy)

Journal-ref: EPTCS 182, 2015

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[59] arXiv:1504.03386 (cross-list from cs.DB) [pdf, other]

Title: Tractable Query Answering and Optimization for Extensions of Weakly-Sticky Datalog+-

Mostafa Milani, Leopoldo Bertossi

Comments: To appear in Proc. Alberto Mendelzon WS on Foundations of Data Management (AMW15)

Subjects: Databases (cs.DB); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[60] arXiv:1504.03473 (cross-list from cs.SE) [pdf, other]

Title: Towards an I/O Conformance Testing Theory for Software Product Lines based on Modal Interface Automata

Lars Luthmann (TU Braunschweig), Stephan Mennicke (TU Braunschweig), Malte Lochau (TU Darmstadt)

Comments: In Proceedings FMSPLE 2015, arXiv:1504.03014

Journal-ref: EPTCS 182, 2015, pp. 1-13

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[61] arXiv:1504.03475 (cross-list from cs.SE) [pdf, other]

Title: Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules

Thi-Kim-Zung Pham, Catherine Dubois, Nicole Levy

Comments: In Proceedings FMSPLE 2015, arXiv:1504.03014

Journal-ref: EPTCS 182, 2015, pp. 44-55

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[62] arXiv:1504.03476 (cross-list from cs.SE) [pdf, other]

Title: Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking

Maurice H. ter Beek (ISTI-CNR, Pisa, Italy), Axel Legay (Inria, Rennes, France), Alberto Lluch Lafuente (DTU, Lyngby, Denmark), Andrea Vandin (University of Southampton, UK)

Comments: In Proceedings FMSPLE 2015, arXiv:1504.03014

Journal-ref: EPTCS 182, 2015, pp. 56-70

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[63] arXiv:1504.04044 (cross-list from cs.DB) [pdf, other]

Title: FAQ: Questions Asked Frequently

Mahmoud Abo Khamis, Hung Q. Ngo, Atri Rudra

Subjects: Databases (cs.DB); Data Structures and Algorithms (cs.DS); Logic in Computer Science (cs.LO)

[64] arXiv:1504.04181 (cross-list from cs.CC) [pdf, other]

Title: Constraint Satisfaction Problems around Skolem Arithmetic

Christian Glasser, Peter Jonsson, Barnaby Martin

Subjects: Computational Complexity (cs.CC); Logic in Computer Science (cs.LO)

[65] arXiv:1504.04768 (cross-list from cs.CR) [pdf, other]

Title: Partial Order Reduction for Security Protocols

David Baelde, Stéphanie Delaune, Lucca Hirschi

Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)

[66] arXiv:1504.04802 (cross-list from cs.AI) [pdf, other]

Title: Gradual Classical Logic for Attributed Objects - Extended in Re-Presentation

Ryuta Arisaka

Comments: arXiv admin note: substantial text overlap with arXiv:1404.6036

Subjects: Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)

[67] arXiv:1504.05018 (cross-list from cs.PL) [pdf, other]

Title: Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions

Amir M. Ben-Amram, Samir Genaim

Comments: Technical report for a corresponding CAV'15 paper

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[68] arXiv:1504.05150 (cross-list from cs.AI) [pdf, other]

Title: Computing Horn Rewritings of Description Logics Ontologies

Mark Kaminski, Bernardo Cuenca Grau

Comments: 15 pages. To appear in IJCAI-15

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[69] arXiv:1504.05513 (cross-list from cs.FL) [pdf, other]

Title: Timed Orchestration for Component-based Systems

Chih-Hong Cheng, Lacramioara Astefanoaei, Harald Ruess, Souha Ben Rayana, Saddek Bensalem

Comments: Timestamp of the work, with evaluation added by creating MES orchestration examples. (v3): typo fix and bring back definition and citation in en^t as in v1

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC)

[70] arXiv:1504.06766 (cross-list from cs.MA) [pdf, other]

Title: Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources

Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi

Subjects: Multiagent Systems (cs.MA); Logic in Computer Science (cs.LO)

[71] arXiv:1504.07702 (cross-list from math.OC) [pdf, other]

Title: Mode-Target Games: Reactive Synthesis for Control Applications

Ayca Balkan, Moshe Vardi, Paulo Tabuada

Comments: This version is an extension of the conference version of the original paper titled "Controller Synthesis for Mode-Target Games"

Subjects: Optimization and Control (math.OC); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO); Systems and Control (eess.SY)

[72] arXiv:1504.07753 (cross-list from cs.DM) [pdf, other]

Title: Hydras: Directed Hypergraphs and Horn Formulas

Robert H. Sloan, Despina Stasi, Gyorgy Turan

Comments: 17 pages, 4 figures

Subjects: Discrete Mathematics (cs.DM); Logic in Computer Science (cs.LO); Combinatorics (math.CO)

[73] arXiv:1504.08108 (cross-list from cs.AI) [pdf, other]

Title: Verification of Generalized Inconsistency-Aware Knowledge and Action Bases (Extended Version)

Diego Calvanese, Marco Montali, Ario Santoso

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)