27 citations · 73 across the 13 of their papers we have counts for
17 papers
Explorations in Subexponential Non-associative Non-commutative Linear Logic
Eben Blaisdell, Max Kanovich, Stepan L. Kuznetsov +2
In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here,…
Explorations in Subexponential non-associative non-commutative Linear Logic (extended version)
Eben Blaisdell, Max I. Kanovich, Stepan L. Kuznetsov +2
In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here,…
On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam +2
This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified usin…
The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities
Max Kanovich, Stepan Kuznetsov, Andre Scedrov
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent…
Language Models for Some Extensions of the Lambek Calculus
Max Kanovich, Stepan Kuznetsov, Andre Scedrov
We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For…
Compliance in Real Time Multiset Rewriting Models
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam +2
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of complia…
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version)
James Brotherston, Max Kanovich
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation…
Subexponentials in non-commutative linear logic
Max Kanovich, Stepan Kuznetsov, Vivek Nigam +1
Linear logical frameworks with subexponentials have been used for the specification of among other systems, proof systems, concurrent programming languages and linear authorization…
Simulating Linear Logic in 1-Only Linear Logic
Max Kanovich
Linear Logic was introduced by Girard as a resource-sensitive refinement of classical logic. It turned out that full propositional Linear Logic is undecidable (Lincoln, Mitchell, S…
A polynomial time algorithm for the Lambek calculus with brackets of bounded order
Max Kanovich, Stepan Kuznetsov, Glyn Morrill +1
Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm fo…
Time, Computational Complexity, and Probability in the Analysis of Distance-Bounding Protocols
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam +2
Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into a…
Undecidability of the Lambek calculus with subexponential and bracket modalities
Max Kanovich, Stepan Kuznetsov, Andre Scedrov
The Lambek calculus is a well-known logical formalism for modelling natural language syntax. The original calculus covered a substantial number of intricate natural language phenom…
Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
Max Kanovich, Stepan Kuznetsov, Andre Scedrov
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called "Lambek's…
Biabduction (and Related Problems) in Array Separation Logic
James Brotherston, Nikos Gorogiannis, Max Kanovich
We investigate array separation logic (ASL), a variant of symbolic-heap separation logic in which the data structures are either pointers or arrays, i.e., contiguous blocks of allo…
Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam +2
Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are oft…
Undecidability of the Lambek calculus with a relevant modality
Max Kanovich, Stepan Kuznetsov, Andre Scedrov
Morrill and Valentin in the paper "Computational coverage of TLG: Nonlinearity" considered an extension of the Lambek calculus enriched by a so-called "exponential" modality. This…
Horn Linear Logic and Minsky Machines
Max Kanovich
Here we give a detailed proof for the crucial point in our Minsky machine simulation - that any linear logic derivation for a specific Horn sequent can be transformed into a Minsky…