Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
6
datasets available to search
ShareScore release 0.9.0
Dataset results
6 results for “LTL”
A SAT Benchmark Suite for LTL Specification Sketching
<h1>LTL_Sketcher-SAT_Benchmark</h1> <p>This repository contains a set of formulas in Propositional Boolean Logic.<br>These formulas are generated during the execution of our <a href="https://github.com/rajarshi008/LTLSketcher/tree/master" target="_blank" rel="noopener">LTLSketcher tool</a>.<br>Given an LTL sketch (i.e., a partial LTL formula) and a sample (i.e., a set of program executions labeled desired and undesired), the tool solves the LTL sketching problem, i.e., complete the sketch to a specification consistent with the data. (feel freet to check out our <a href="https://link.springer.com/chapter/10.1007/978-3-031-45332-8_2" target="_blank" rel="noopener">paper</a> for more information on this problem)<br>In essence, this is done by reducing the problem to a series of formulas in Propositional Boolean Logic and checking their satisfiability.</p> <h2>Naming convention:</h2> <p>This repository contains each formula both in the DIMACS and SMTLib format.<br>Each file follows the same naming convention:</p> <p><em>type__sample-file__sketch__size__algorithm-configuration__satisifability</em></p> <p><em>type</em>: indicates whether the formula is stored in the DIMACS or SMTLib format<br><em>sample-file</em>: refers to the sample (cf., <a href="https://github.com/rajarshi008/LTLSketcher/tree/master/experiment_results/generated_files/final_benchmark" target="_blank" rel="noopener">here</a>) used by the LTLSketcher tool<br><em>sketch</em>: refers to the sketch (cf., See experimental evaluation of our <a href="https://link.springer.com/chapter/10.1007/978-3-031-45332-8_2" target="_blank" rel="noopener">paper</a>) used by the LTLSketcher tool<br><em>size</em>: refers to the size of the complete solution (i.e., the number of subformulas of the complete specification)<br><em>algorithm-configuration</em>: our algorithm can be extended by two heuristics (BMC and suffix), this indicates which combination of heuristics was used (none, either one of the two, both)<br><em>satisfiability</em>: indicates whether the formula is satisfiable or not</p>
Accepted Artifact for Little Tricky Logic: Misconceptions in the Understanding of LTL
<p>Datasets and source materials for our studies of Linear Temporal Logic (LTL).</p> <p>Includes:</p> <ul> <li> <p> Labelled responses to our surveys</p> </li> <li> <p>The surveys themselves</p> </li> <li> <p>The coding rubric that guided our categorization</p> </li> </ul>
Reproducibility Package: Automata-Driven Partial Order Reduction and Guided Search for LTL
<p>Reproducibility package for the paper <strong>Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking</strong> accepted for VMCAI'22.</p> <p>Contains scripts, 64-bit Linux binaries, and the dataset used to run the experiments detailed in the paper, a source code snapshot used to compile those binaries, as well as scripts for processing the results into the tables seen in the paper. The file README.md contains details on running the various parts of the artifacts, assuming a Linux environment.</p>
How Bit-Vector Logic Can Help Improve the Verification of First-Order LTL Specifications
<p>Experimental evaluation for the encoding presented in the paper "How Bit-Vector Logic Can Help Improve the Verification of First-Order LTL Specifications".</p> <p>The encoding is implemented as a zot plugin entitled ae2bvzot.</p>
Artefact for paper "LTL under reductions with weaker conditions than stutter-invariance"
<p><strong>LTLSensitivityToLength : LTL artefacts on length-sensitivity</strong></p> <p>Procedures and artefacts to reproduce experiments on "length" sensitivity of LTL formulas.</p> <p>We use both Tapaal <a href="https://www.tapaal.net/">https://www.tapaal.net/</a> and ITS-Tools <a href="https://lip6.github.io/ITSTools-web/">https://lip6.github.io/ITSTools-web/</a> in these experiments on models taken from the model-checking competition 2021 <a href="https://mcc.lip6.fr/">https://mcc.lip6.fr/</a>.</p> <p>See also companion GitHub project here : https://github.com/yanntm/LTLSensitivityToLength/</p> <p><strong>Workflow and steps</strong></p> <p>Please refer to the source of the "~/demo.sh" file for more details on the different steps.</p> <ul> <li>Step 0 : download the VM provided by the conference from here : <a href="https://zenodo.org/record/5562597">https://zenodo.org/record/5562597</a> Click the ".ova" to download the VM then open it and start it with VirtualBox.</li> <li>Step 1 : login to the VM with user/pass : tacas22/tacas22. You can change keyboard setting by doing : right click background, Display Setting, left in "Region & Language", "Input sources", first "Add" French/your keyboard type (it is in "other") then trash "US-en" using the garbage can icon. Right-click background->"Open in terminal" will now give us a terminal with correct keyboard.</li> <li>Step 2 : Download and deploy artefact in the VM. Use the Zenodo link at the bottom of this page to download and place it at the root of the tacas22 home: in /home/tacas22/. Then deploy with tar xvzf home.tgz.</li> <li>Step 3 : There are several Readme with more details but the rest is done using the demo.sh so simply run it. It will enact the further steps.</li> </ul> <p><strong>Steps in the demo</strong></p> <p>Much more detail is available in the ~/demo.sh file.</p> <ul> <li>Step 0 : install debian dependencies. We use R language and modern Java.</li> <li>Step 1 : Analyze sensitivity to length of LTL formulas and compute reduced models. This step is handled by ITS-tools. Because the benchmark is so huge we only reproduce using three model instances (out of 2822). More examples can be run by editing "step 1" of demo.sh to add more runs.</li> <li>Step 2 : run an MCC model-checker with both reduced and original model/formula pairs. Collect logs and compute a CSV summary file from these raw logs. We run both Tapaal and ITS-Tools. We did our best to simulate the conditions we ran in (we capture output in OAR.XX.out and OAR.XX.err files), but we use a cluster and OAR to reserve cpu on it in the full experiment so the match is not perfect. The actual scripts we used on the cluster are also part of this distribution however.</li> <li>Step 3 : build tables from the CSV and formulas of literature on sensitivity to length in practice. This corresponds to the Table in section 4.1 of the paper. For a large set of formulas we compute whether it is stutter insensitive, shortening insensitive, lengthening insensitive, or arbitrary. This step can actually be performed after or before Step 2 it only depnds on data produced at step 1.</li> <li>Step 4 : build tables and plots from the CSV of Step 2 using R. The demo script builds both the plots using the data you have just collected at step 1 and using the full data from our experiment. To make these auditable, we provide the CSV resulting from our cluster run in ~/tacas22/Rscripts/clusterLog as well as all the logs of this run in the ~/tacas22/logsCluster.tgz that were parsed to build the CSV.</li> </ul> <p><strong>Contents</strong></p> <p>We have deployed all dependencies.</p> <ul> <li>~/usr/ contains local installations of the LTL manipulation library Spot and of libraried required for R (used in analysis)</li> <li>~/tapaal/ contains Tapaal, configured for MCC mode. It was built from the bzr depot of Tapaal from source, following instructions helpfully provided by the authors Jiri Srba et al.</li> <li>~/tacas22/Spot-Binary-Builds/ is the folder used to build Spot with appropriate flags. We used "build_cluster.sh" script. You do not need to do this however it is deployed in ~/usr/local. The companion github is <a href="https://github.com/yanntm/Spot-Binary-Builds">https://github.com/yanntm/Spot-Binary-Builds</a>.</li> <li>~/tacas22/packages/ contains the apt-get debian packages needed to run our demo. Essentially we need R language and Java language support.</li> </ul> <p>There are instructions on how to rebuild these dependencies from scratch in each subfolder. Again it is not necessary to do so with the provided archive.</p> <p>Then the tools/models :</p> <ul> <li>~/tacas22/ITS-Tools-MCC contains the ITS-Tools distribution as well as the inputs from the MCC'21 edition. Both of these are extracted and installed following the instruction on the three github : <a href="https://github.com/yanntm/pnmcc-models-2021">https://github.com/yanntm/pnmcc-models-2021</a> (curated/annotated models from MCC 21) <a href="https://github.com/yanntm/pnmcc-tests">https://github.com/yanntm/pnmcc-tests</a> (For the test/runner framework) <a href="https://github.com/yanntm/ITS-Tools-MCC">https://github.com/yanntm/ITS-Tools-MCC</a> (For ITS-tools distributed for the MCC)</li> <li>~/tacas22/LTLPatterns/ contains formulas collected from the literature as well as a script to analyze their sensitiivty and compute metrics on them. See the README in that folder for more details.</li> <li>~/tacas22/Rscripts/ contains scripts to analyze the results and produce plots used in the paper. See the README in that folder for more details. It also contains the CSV produced from our cluster run (in clusterLog/) to reproduce the plots (these were built using the full logs provided in ~/tacas22/logsCluster.tgz and analyzed with the perl scripts from the ~/tacas22/ITS-Tools-MCC folder)</li> </ul> <p>The requirements for this setup include:</p> <ul> <li>A version of Spot : <a href="https://spot.lrde.epita.fr/">https://spot.lrde.epita.fr/</a> to both translate LTL to an automaton and analyze its sensitivity.</li> <li>The models and formulas from the <a href="https://mcc.lip6.fr/">Model Checking Contest 2021</a>. We grab these from our <a href="https://github.com/yanntm/pnmcc-models-2021">PNMCC Models 2021</a> repository that itself builds the files using the official distribution of the MCC.</li> <li>Our test/runner framework for these examples, available from <a href="https://github.com/yanntm/pnmcc-tests">https://github.com/yanntm/pnmcc-tests</a></li> </ul> <p>Then we need a MCC compatible tool that can compete in the LTL category of the contest. We used~:</p> <ul> <li>A version of <a href="http://ddd.lip6.fr/">ITS-tools</a> : we use the version packaged for the MCC competition, available from here : <a href="https://github.com/yanntm/ITS-commandline">ITS-tools for MCC</a></li> <li>A version of <a href="https://www.tapaal.net/">Tapaal</a> : we build it from the source repositories with flags to enable MCC mode. See repository here : <a href="https://bazaar.launchpad.net/~verifypn-maintainers/verifypn/new-trunk/files/head:/Scripts/MCC21/competition-scripts">https://bazaar.launchpad.net/~verifypn-maintainers/verifypn/new-trunk/files/head:/Scripts/MCC21/competition-scripts</a> and <a href="https://code.launchpad.net/verifypn">https://code.launchpad.net/verifypn</a></li> </ul> <p><strong>License</strong></p> <p>This work is provided under the terms of GPL v3 or more recent.</p> <p>(C) Yann Thierry-Mieg, Denis Poitrenaud, Etienne Renault, Emmanuel Paviot-Adet. Sorbonne Université, CNRS. 2021.</p>
Diet Quality and LTL in NHANES
ClinicalTrials.gov study NCT03302104. IPD Sharing: Not stated. Countries: 0. Publications: 0.
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.