### Top 10 Arxiv Papers Today in Logic In Computer Science

##### #1. Precondition Inference via Partitioning of Initial States
###### Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J. Stuckey
Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of \emph{safe} and \emph{unsafe} \emph{initial} states. Then we repeatedly use the current abstractions to partition the program's \emph{initial} states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods.
more | pdf | html
None.
###### Tweets
ComputerPapers: Precondition Inference via Partitioning of Initial States. https://t.co/i9zbDuESGm
###### Github

Preconditions inferrer for Horn clauses

Repository: PI-Horn
User: bishoksan
Language: Prolog
Stargazers: 0
Subscribers: 2
Forks: 0
Open Issues: 0
None.
###### Other stats
Sample Sizes : None.
Authors: 5
Total Words: 9466
Unqiue Words: 2161

##### #2. Spatial Logics and Model Checking for Medical Imaging (Extended Version)
###### Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink
Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces -- Closure Spaces being a generalisation of topological spaces, covering also discrete space structures -- and topochecker, a model-checker for SLCS (and extensions thereof). We introduce the logical language ImgQL ("Image Query Language"). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distancebased operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our...
more | pdf | html
###### Tweets
arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
arxivml: "Spatial Logics and Model Checking for Medical Imaging (Extended Version)", Fabrizio Banci Buonamici, Gina Belmonte… https://t.co/blLKoDwmDY
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
ComputerPapers: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/DL0Gtf0GQc
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
Rosenchild: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
bd_gfngfn: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPh9U9N
elazzouzim: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
na4zagin3: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
nakano_muramoto: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
komorin9502: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
Bchoudhury_1: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
SandMouth: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 5
Total Words: 19034
Unqiue Words: 4658

##### #3. Granularity and Generalized Inclusion Functions - Their Variants and Contamination
###### Mani A
Rough inclusion functions (RIFs) are known by many other names in formal approaches to vagueness, belief, and uncertainty. Their use is often poorly grounded in factual knowledge or involve wild statistical assumptions. The concept of contamination introduced and studied by the present author across a number of her papers, concerns mixing up of information across semantic domains (or domains of discourse). RIFs play a key role in contaminating algorithms and some solutions that seek to replace or avoid them have been proposed and investigated by the present author in some of her earlier papers. The proposals break many algorithms of rough sets in a serious way. In this research, algorithm-friendly granular generalizations of such functions that reduce contamination are proposed and investigated from a mathematically sound perspective. Interesting representation results are proved and a core algebraic strategy for generalizing Skowron-Polkowski style of rough mereology is formulated.
more | pdf | html
None.
###### Tweets
arxivml: "Granularity and Generalized Inclusion Functions - Their Variants and Contamination", Mani A https://t.co/Rw3gVHimwq
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 4758
Unqiue Words: 1564

##### #4. Progressive Algorithms for Domination and Independence
###### Grzegorz Fabiański, Michał Pilipczuk, Sebastian Siebertz, Szymon Toruńczyk
We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the distance-r dominating set problem (parameterized by the solution size) in a wide variety of restricted graph classes, such as powers of nowhere dense classes, map graphs, and (for $r=1$) biclique-free graphs. Similarly, for the distance-r independent set problem the technique can be used to give a linear-time fixed-parameter algorithm on any nowhere dense class. Despite the simplicity of the method, in several cases our results extend known boundaries of tractability for the considered problems and improve the best known running times.
more | pdf | html
###### Tweets
MathPaper: Progressive Algorithms for Domination and Independence. https://t.co/o5hWXr5TBQ
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 4
Total Words: 18056
Unqiue Words: 2598

##### #5. Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
###### Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 steps with probability at most 1%." To this goal, we devise a theory of supermartingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those supermartingales. Our experiments suggest the method's practical use.
more | pdf | html
None.
###### Tweets
ComputerPapers: Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments. https://t.co/ojJABUDgqP
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 15815
Unqiue Words: 3205

##### #6. Computing the Expected Execution Time of Probabilistic Workflow Nets
###### Philipp J. Meyer, Javier Esparza, Philip Offtermatt
Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of "earliest-first" schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P-hard, and so polynomial algorithms are very unlikely to exist. Further, #P-hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite...
more | pdf | html
None.
###### Tweets
ComputerPapers: Computing the Expected Execution Time of Probabilistic Workflow Nets. https://t.co/p89RQBZn7Z
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 15074
Unqiue Words: 2550

##### #7. Revisiting the generalized Łoś-Tarski theorem
###### Abhisekh Sankaran
We present a new proof of the generalized {\L}o\'s-Tarski theorem ($\mathsf{GLT}(k)$) introduced in [1], over arbitrary structures. Instead of using $\lambda$-saturation as in [1], we construct just the "required saturation" directly using ascending chains of structures. We also strengthen the failure of $\mathsf{GLT}(k)$ in the finite shown in [2], by strengthening the failure of the {\L}o\'s-Tarski theorem in this context. In particular, we prove that not just universal sentences, but for each fixed $k$, even $\Sigma^0_2$ sentences containing $k$ existential quantifiers fail to capture hereditariness in the finite. We conclude with two problems as future directions, concerning the {\L}o\'s-Tarski theorem and $\mathsf{GLT}(k)$, both in the context of all finite structures. [1] 10.1016/j.apal.2015.11.001 ; [2] 10.1007/978-3-642-32621-9\_22
more | pdf | html
None.
###### Tweets
ComputerPapers: Revisiting the generalized {\L}o\'s-Tarski theorem. https://t.co/GGGCzQbMCH
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVdRHkx
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVdRHkx
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVe9iJ7
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 7371
Unqiue Words: 1370

##### #8. Jets and differential linear logic
###### James Wallbridge
We prove that the category of vector bundles over a fixed smooth manifold and its corresponding functional analytic category of convenient modules are models for intuitionistic differential linear logic in two ways. The first uses the jet comonad to model the exponential modality. In this case the Kleisli category is the category of convenient modules with linear differential operators as morphisms. The second uses the more familiar distributional comonad whose Kleisli category is the category of convenient modules and smooth morphisms. Combining the two gives a new interpretation of the semantics of differential linear logic where the Kleisli morphisms are smooth local functionals, or equivalently, non-linear partial differential operators, and the codereliction map induces the functional derivative. This points towards a logic and hence computational theory of non-linear partial differential equations and their solutions based on variational calculus.
more | pdf | html
None.
###### Tweets
ComputerPapers: Jets and differential linear logic. https://t.co/4eD68U6jke
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHwaeo
danielmurfet: RT @arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
JosephJohnCox: RT @arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 13202
Unqiue Words: 2346

##### #9. Verified Runtime Validation for Partially Observable Hybrid Systems
###### Stefan Mitsch, Andre Platzer
Formal verification provides strong safety guarantees about models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation. The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor...
more | pdf | html
None.
###### Tweets
ComputerPapers: Verified Runtime Validation for Partially Observable Hybrid Systems. https://t.co/Y6CcAgJTY9
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV742ck
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV742ck
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV6MrkM
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 2
Total Words: 12138
Unqiue Words: 2850

##### #10. On the specification and verification of atomic swap smart contracts
###### Ron van der Meyden
Blockchain systems and smart contracts provide ways to securely implement multi-party transactions without the use of trusted intermediaries, which currently underpin many commercial transactions. However, they do so by transferring trust to computer systems, raising the question of whether code can be trusted. Experience with high value losses resulting from incorrect code has already shown that formal verification of smart contracts is likely to be beneficial. This note investigates the specification and verification of a simple form of multi-party transaction, atomic swaps. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, for our specific examples, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through a number of examples of the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.
more | pdf | html
None.
###### Tweets
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFwKmON
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFwKmON
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFx1Ydn
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 10089
Unqiue Words: 2294

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

Tracking 58,338 papers.

###### Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Online
###### Stats
Tracking 58,338 papers.