Logic in Computer Science

New submissions

• New submissions
• Cross-lists
• Replacements

New submissions for Fri, 10 May 24

[1]  arXiv:2405.05546 [pdf, other]

Title: Data reification in a concurrent rely-guarantee algebra

Authors: Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones

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

Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic theory supporting rely-guarantee reasoning about concurrency. A concurrent version of the Galler-Fischer equivalence relation data structure is used as an example.

[2]  arXiv:2405.05670 [pdf, ps, other]

Title: Between proof construction and SAT-solving

Authors: Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski

Subjects: Logic in Computer Science (cs.LO)

The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (with all connectives) can be reduced to provability of implicational formulas of order three. Another advantage is a convenient interpretation in terms of simple alternating automata. Additionally, we distinguish some natural subclasses of IIPC corresponding to the complexity classes NP and co-NP. Our experimental results show that a simple decision procedure requires a significant amount of time only in a small fraction of cases.

[3]  arXiv:2405.05690 [pdf, other]

Title: Restructuring a concurrent refinement algebra

Authors: Ian J. Hayes, Larissa A. Meinicke, Naso Evangelou-Oost

Subjects: Logic in Computer Science (cs.LO)

The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is added via compatible sets of commands, including tests, atomic commands and pseudo-atomic commands. These allow stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.

Cross-lists for Fri, 10 May 24

[4]  arXiv:2405.05774 (cross-list from math.CT) [pdf, ps, other]

Title: Monoidal bicategories, differential linear logic, and analytic functors

Authors: M. Fiore, N. Gambino, M. Hyland

Comments: v1. 46 pages. Comments welcome

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

We develop further the theory of monoidal bicategories by introducing and studying bicate- gorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of Joyal's analytic functors to analytic functors between presheaf categories, just as ordinary calculus extends from a single variable to many variables.

[5]  arXiv:2405.05962 (cross-list from cs.LG) [pdf, other]

Title: Age Aware Scheduling for Differentially-Private Federated Learning

Authors: Kuan-Yu Lin, Hsuan-Yin Lin, Yu-Pin Hsu, Yu-Chih Huang

Comments: "Paper accepted to the 2024 IEEE International Symposium on Information Theory (ISIT)"

Subjects: Machine Learning (cs.LG); Information Theory (cs.IT); Logic in Computer Science (cs.LO)

This paper explores differentially-private federated learning (FL) across time-varying databases, delving into a nuanced three-way tradeoff involving age, accuracy, and differential privacy (DP). Emphasizing the potential advantages of scheduling, we propose an optimization problem aimed at meeting DP requirements while minimizing the loss difference between the aggregated model and the model obtained without DP constraints. To harness the benefits of scheduling, we introduce an age-dependent upper bound on the loss, leading to the development of an age-aware scheduling design. Simulation results underscore the superior performance of our proposed scheme compared to FL with classic DP, which does not consider scheduling as a design factor. This research contributes insights into the interplay of age, accuracy, and DP in federated learning, with practical implications for scheduling strategies.

Replacements for Fri, 10 May 24

[6]  arXiv:2304.09639 (replaced) [pdf, ps, other]

Title: The Transformation Logics

Authors: Alessandro Ronca

Comments: Extended version with appendix of a paper with the same title that will appear in the proceedings of IJCAI 2024

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

[7]  arXiv:2306.01466 (replaced) [pdf, other]

Title: On the Complexity of Proving Polyhedral Reductions

Authors: Nicolas Amat (IMDEA Software Institute), Silvano Dal Zilio (LAAS-VERTICS, LAAS), Didier Le Botlan (LAAS-VERTICS, LAAS)

Subjects: Logic in Computer Science (cs.LO)

[8]  arXiv:2403.01954 (replaced) [pdf, other]

Title: DECIDER: A Rule-Controllable Decoding Strategy for Language Generation by Imitating Dual-System Cognitive Theory

Authors: Chen Xu, Tian Lan, Changlong Yu, Wei Wang, Jun Gao, Yu Ji, Qunxi Dong, Kun Qian, Piji Li, Wei Bi, Bin Hu

Comments: Submitted to IEEE TKDE (Major Revision), 12 pages, 6 figures

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

• New submissions
• Cross-lists
• Replacements