{"id":"W2117444225","doi":"10.1109/ispass.2008.4510741","title":"Performance Analysis of ARQ Protocols using a Theorem Prover","year":2008,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":16,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Automatic repeat request; HOL; Selective Repeat ARQ; Sliding window protocol; Automated theorem proving; Hybrid automatic repeat request; Protocol (science); Transmission (telecommunications); Go-Back-N ARQ; Theoretical computer science; Algorithm; Programming language; Window (computing); Telecommunications","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006751145,0.001088254,0.0009377241,0.001546307,0.0007382425,0.002370433,0.002100209,0.001116983,0.002763679],"category_scores_gemma":[0.01821052,0.0005650535,0.001479457,0.0009436026,0.001890918,0.003333883,0.001312997,0.001519737,0.0004127013],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002702614,"about_ca_system_score_gemma":0.002393272,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001884472,"about_ca_topic_score_gemma":0.001063712,"domain_scores_codex":[0.9927561,0.002728839,0.0003819777,0.0006936216,0.002690881,0.0007486696],"domain_scores_gemma":[0.9731494,0.02176534,0.001337511,0.00204841,0.001511987,0.0001874739],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0004673225,0.0004833061,0.004204105,0.0004408419,0.0001541106,0.0004313985,0.000339746,0.69419,0.02522337,0.2335712,0.001478706,0.03901597],"study_design_scores_gemma":[0.00004287673,0.00009788363,0.0001630889,0.000009882578,0.00002728935,0.00004462197,0.00001626382,0.9667889,0.009958702,0.02231412,0.0005231429,0.00001317964],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.07151371,0.0001643341,0.9214247,0.0002701242,0.00003599737,0.0001231738,0.0001842495,0.002543327,0.003740469],"genre_scores_gemma":[0.8307799,0.0002835995,0.1665853,0.0001383184,0.00006726268,0.0001848177,0.0002384078,0.0002737204,0.001448712],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.006751145,"threshold_uncertainty_score":0.0357039,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09979860810567057,"score_gpt":0.3531336525605817,"score_spread":0.2533350444549111,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}