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.
7
datasets available to search
ShareScore release 0.9.0
Dataset results
7 results for “timed automata”
Data for paper "Efficient Convex Zone Merging in Parametric Timed Automata"
<p>This is the experimental data for paper "Efficient Convex Zone Merging in Parametric Timed Automata"</p> <p>It comes in the form of two archives:</p> <ol> <li><strong>merging-artifact.zip</strong>: the whole set of benchmarks with the scripts to run</li> <li><strong>merging-artifact-FORMATS22-results.zip</strong>: all results executed 5 times</li> </ol>
The IMITATOR benchmarks library 2.1: A benchmarks library for extended parametric timed automata
<p>We present here the IMITATOR benchmarks library 2.1: A benchmarks library for extended parametric timed automata</p> <p> </p> <p>We present two archives:</p> <p>- one (benchmarks.zip) with the models and the properties</p> <p>- one (full.zip) with the benchmarks and all the results: the expected results, generated PDF and graphics, and a whole standalone Web page (more or less equivalent to <a href="https://www.imitator.fr/static/library.html">www.imitator.fr/static/library.html</a>) summarizing all benchmarks</p> <p> </p> <p>See a full description in the TAP 2021 paper ("<a href="https://link.springer.com/10.1007/978-3-030-79379-1_3">A Benchmarks Library for Extended Parametric Timed Automata</a>")</p>
Data for paper "Zone extrapolations in parametric timed automata"
<p>Data for paper "<em>Zone extrapolations in parametric timed automata</em>"</p> <p>This data set comes with two zip files:</p> <ol> <li><strong>artifact.zip</strong> contains the current version of IMITATOR, all models and necessary scripts to reproduce all experiments on our benchmarks set. A file named README.md gives all instructions for reproducibility.</li> <li><strong>results.zip</strong> contains an HTML page with a table summarizing all results, and all raw results (.res) as well.</li> </ol> <p> </p>
Experimental data for Distributed parametric model checking timed automata under non-Zenoness assumption
<p>This is the experimental data mentioned in the paper "Distributed parametric model checking timed automata under non-Zenoness assumption", published in FMSD (Formal Methods in System Design), 2022.</p> <p>Experiments were conducted using the distributed version of IMITATOR 2.9.2 (Butter Incaberry) on two Intel Xeon Silver 4114 at 2.2GHz (20 cores in total), and 96GiB of memory, running under Ubuntu 16.04 LTS 64-bit.</p>
Supplementary Material for the Paper "Configurable Verification of Timed Automata with Discrete Variables"
<p>The tool we used for producing the experimental data is implemented as a prototype in the open source model checking framework <a href="http://theta.inf.mit.bme.hu">Theta</a>. Source code is available on <a href="https://github.com/FTSRG/theta">GitHub</a>. The experimental data is based on <a href="https://github.com/FTSRG/theta/tree/be86f967998b7065cd55cb629322bffd8333af54">this commit</a>.</p> <p><strong>Prerequisites</strong></p> <p><a href="https://www.oracle.com/technetwork/java/javase/downloads/jdk11-downloads-5066655.html">Java SE Runtime Environment 11</a></p> <p><strong>Building the tool</strong></p> <p>See the <a href="http://github.com/ftsrg/theta/blob/be86f967998b7065cd55cb629322bffd8333af54/hu.bme.mit.theta.xta/README.md">build instructions</a>.</p> <p><strong>Usage</strong></p> <pre><code> $ java -jar theta-xta-cli.jar --clock <LU|FWITP|BWITP> Refinement strategy for clock variables --discrete <NONE|FWITP|BWITP> Refinement strategy for clock variables --model <MODEL> Path of the input model --search <BFS|DFS|RANDOM> Search strategy </code> </pre> <p><strong>Example</strong></p> <pre><code> $ java -jar theta-xta-cli.jar --model models\c1.xta --clock FWITP --discrete BWITP --search DFS </code> </pre> <p><strong>Sample output</strong></p> <pre><code> AlgorithmTimeInMs: 3482 // Total execution time in ms ExpandTimeInMs: 2128 // Time spend with expansion in ms CloseTimeInMs: 1301 // Time spent with covering nodes in ms ExpandExplRefinementTimeInMs: 901 // Expand refinement time for explicit domain in ms ExpandZoneRefinementTimeInMs: 84 // Expand refinement time for zone domain in ms CloseExplRefinementTimeInMs: 890 // Close refinement time for explicit domain in ms CloseZoneRefinementTimeInMs: 145 // Close refinement time for zone domain in ms CoverageChecks: 628201 // Number of coverage checks CoverageAttempts: 6069 // Number of attempts for forced coverage CoverageSuccesses: 6065 // Number of successes for forced coverage ExplRefinementSteps: 33560 // Number of refinements steps for explicit domain ZoneRefinementSteps: 1544 // Number of refinements steps for zone domain ArgDepth: 879 // Depth of the reachability graph ArgNodes: 14973 // Number of nodes in the reachability graph ArgNodesExpanded: 9307 // Number of expanded nodes in the reachability graph </code> </pre> <p>For the experiments, we used JVM switches <code>-Xmx6G</code> and <code>-Xss8m</code>.</p>
Artefact for: "Optimal Infinite Temporal Planning: Cyclic Plans for Priced Timed Automata"
<p>This artefact contains the UPPAAL models and raw data from experiments for the paper.</p>
Artifact for paper "Monte Carlo Tree Search for Priced Timed Automata"
<p>Artifact for paper "Monte Carlo Tree Search for Priced Timed Automata"</p>
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.